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  6612  fcof  6691  brinxper  8673  mapdom2  9086  fisupg  9198  fiint  9237  dffi3  9344  fiinfg  9414  dfac2b  10053  nnadju  10120  cflm  10172  cfslbn  10189  cardmin  10486  fpwwe2lem11  10564  fpwwe2lem12  10565  elfznelfzob  13729  modsumfzodifsn  13906  dvdsdivcl  16285  isprm5  16677  latjlej1  18419  latmlem1  18435  chnccat  18592  cnrest2  23251  cnpresti  23253  trufil  23875  stdbdxmet  24480  lgsdir  27295  elwwlks2  30037  orthin  31517  mdbr2  32367  dmdbr2  32374  mdsl2i  32393  atcvat4i  32468  mdsymlem3  32476  tz9.1regs  35278  wzel  36004  ontgval  36613  poimirlem3  37944  poimirlem4  37945  poimirlem29  37970  poimir  37974  suceldisj  39139  cmtbr4N  39701  cvrat4  39889  cdlemblem  40239  negexpidd  43114  3cubeslem1  43116  tfsconcatb0  43772  ensucne0OLD  43957  itschlc0xyqsol  49243  elpglem2  50187