Theorem jctird 526

Description: Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

Ref	Expression
jctird.1	⊢ (𝜑 → (𝜓 → 𝜒))
jctird.2	⊢ (𝜑 → 𝜃)

Assertion

Ref	Expression
jctird	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Proof of Theorem jctird

Step	Hyp	Ref	Expression
1		jctird.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jctird.2	. . 3 ⊢ (𝜑 → 𝜃)
3	2	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 512	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  anc2ri  556  pm5.31  830  fnun  6662  fcof  6740  fcoOLD  6742  mapdom2  9166  fisupg  9309  fiint  9342  dffi3  9448  fiinfg  9516  dfac2b  10147  nnadju  10214  cflm  10267  cfslbn  10284  cardmin  10581  fpwwe2lem11  10658  fpwwe2lem12  10659  elfznelfzob  13764  modsumfzodifsn  13935  dvdsdivcl  16286  isprm5  16671  latjlej1  18438  latmlem1  18454  cnrest2  23183  cnpresti  23185  trufil  23807  stdbdxmet  24417  lgsdir  27258  elwwlks2  29770  orthin  31249  mdbr2  32099  dmdbr2  32106  mdsl2i  32125  atcvat4i  32200  mdsymlem3  32208  wzel  35414  ontgval  35909  poimirlem3  37090  poimirlem4  37091  poimirlem29  37116  poimir  37120  cmtbr4N  38721  cvrat4  38910  cdlemblem  39260  negexpidd  42096  3cubeslem1  42098  tfsconcatb0  42767  ensucne0OLD  42954  gricer  47184  itschlc0xyqsol  47834  elpglem2  48137

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »