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 207  df-an 396

This theorem is referenced by:  anc2ri  556  pm5.31  830  fnun  6693  fcof  6770  fcoOLD  6772  brinxper  8792  mapdom2  9214  fisupg  9352  fiint  9394  fiintOLD  9395  dffi3  9500  fiinfg  9568  dfac2b  10200  nnadju  10267  cflm  10319  cfslbn  10336  cardmin  10633  fpwwe2lem11  10710  fpwwe2lem12  10711  elfznelfzob  13823  modsumfzodifsn  13995  dvdsdivcl  16364  isprm5  16754  latjlej1  18523  latmlem1  18539  cnrest2  23315  cnpresti  23317  trufil  23939  stdbdxmet  24549  lgsdir  27394  elwwlks2  29999  orthin  31478  mdbr2  32328  dmdbr2  32335  mdsl2i  32354  atcvat4i  32429  mdsymlem3  32437  wzel  35788  ontgval  36397  poimirlem3  37583  poimirlem4  37584  poimirlem29  37609  poimir  37613  cmtbr4N  39211  cvrat4  39400  cdlemblem  39750  negexpidd  42638  3cubeslem1  42640  tfsconcatb0  43306  ensucne0OLD  43492  itschlc0xyqsol  48501  elpglem2  48804