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  6683  fcof  6763  brinxper  8785  mapdom2  9205  fisupg  9317  fiint  9356  dffi3  9460  fiinfg  9530  dfac2b  10248  nnadju  10315  cflm  10366  cfslbn  10384  cardmin  10687  fpwwe2lem11  10765  fpwwe2lem12  10766  elfznelfzob  13949  modsumfzodifsn  14127  dvdsdivcl  16530  isprm5  16927  latjlej1  18677  latmlem1  18693  chnccat  18850  cnrest2  23659  cnpresti  23661  trufil  24284  stdbdxmet  24889  lgsdir  27716  elwwlks2  30615  orthin  32105  mdbr2  32955  dmdbr2  32962  mdsl2i  32981  atcvat4i  33056  mdsymlem3  33064  rmo6  35821  fnfvintima  35827  mpofvd  35838  tz9.1regs  35943  j0ltaleph  36049  wzel  36801  ontgval  37434  poimirlem3  38809  poimirlem4  38810  poimirlem29  38835  poimir  38839  suceldisj  40016  cmtbr4N  40578  cvrat4  40766  cdlemblem  41116  negexpidd  43958  3cubeslem1  43960  tfsconcatb0  44607  ensucne0OLD  44792  itschlc0xyqsol  50210  elpglem2  51211