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  6647  fcof  6727  brinxper  8727  mapdom2  9147  fisupg  9259  fiint  9297  dffi3  9402  fiinfg  9472  dfac2b  10134  nnadju  10201  cflm  10252  cfslbn  10270  cardmin  10573  fpwwe2lem11  10651  fpwwe2lem12  10652  elfznelfzob  13831  modsumfzodifsn  14009  dvdsdivcl  16407  isprm5  16799  latjlej1  18542  latmlem1  18558  chnccat  18715  cnrest2  23512  cnpresti  23514  trufil  24137  stdbdxmet  24742  lgsdir  27569  elwwlks2  30438  orthin  31928  mdbr2  32778  dmdbr2  32785  mdsl2i  32804  atcvat4i  32879  mdsymlem3  32887  fnfvintima  35592  tz9.1regs  35661  wzel  36402  ontgval  37051  poimirlem3  38373  poimirlem4  38374  poimirlem29  38399  poimir  38403  suceldisj  39567  cmtbr4N  40129  cvrat4  40317  cdlemblem  40667  negexpidd  43528  3cubeslem1  43530  tfsconcatb0  44186  ensucne0OLD  44371  itschlc0xyqsol  49698  elpglem2  50639