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  831  fnun  6682  fcof  6759  brinxper  8774  mapdom2  9188  fisupg  9324  fiint  9366  fiintOLD  9367  dffi3  9471  fiinfg  9539  dfac2b  10171  nnadju  10238  cflm  10290  cfslbn  10307  cardmin  10604  fpwwe2lem11  10681  fpwwe2lem12  10682  elfznelfzob  13812  modsumfzodifsn  13985  dvdsdivcl  16353  isprm5  16744  latjlej1  18498  latmlem1  18514  cnrest2  23294  cnpresti  23296  trufil  23918  stdbdxmet  24528  lgsdir  27376  elwwlks2  29986  orthin  31465  mdbr2  32315  dmdbr2  32322  mdsl2i  32341  atcvat4i  32416  mdsymlem3  32424  wzel  35825  ontgval  36432  poimirlem3  37630  poimirlem4  37631  poimirlem29  37656  poimir  37660  cmtbr4N  39256  cvrat4  39445  cdlemblem  39795  negexpidd  42693  3cubeslem1  42695  tfsconcatb0  43357  ensucne0OLD  43543  itschlc0xyqsol  48688  elpglem2  49231