Theorem jctird 536

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 26	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 522	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anc2ri  566  pm5.31  844  fnun  6653  fcof  6733  brinxper  8747  mapdom2  9167  fisupg  9279  fiint  9318  dffi3  9423  fiinfg  9493  dfac2b  10209  nnadju  10276  cflm  10327  cfslbn  10345  cardmin  10648  fpwwe2lem11  10726  fpwwe2lem12  10727  elfznelfzob  13909  modsumfzodifsn  14087  dvdsdivcl  16486  isprm5  16883  latjlej1  18627  latmlem1  18643  chnccat  18800  cnrest2  23604  cnpresti  23606  trufil  24229  stdbdxmet  24834  lgsdir  27659  elwwlks2  30558  orthin  32048  mdbr2  32898  dmdbr2  32905  mdsl2i  32924  atcvat4i  32999  mdsymlem3  33007  fnfvintima  35714  tz9.1regs  35802  wzel  36586  ontgval  37219  poimirlem3  38541  poimirlem4  38542  poimirlem29  38567  poimir  38571  suceldisj  39750  cmtbr4N  40312  cvrat4  40500  cdlemblem  40850  negexpidd  43692  3cubeslem1  43694  tfsconcatb0  44345  ensucne0OLD  44530  itschlc0xyqsol  49878  elpglem2  50804