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  8730  mapdom2  9143  fisupg  9255  fiint  9293  dffi3  9398  fiinfg  9468  dfac2b  10130  nnadju  10197  cflm  10248  cfslbn  10266  cardmin  10565  fpwwe2lem11  10643  fpwwe2lem12  10644  elfznelfzob  13822  modsumfzodifsn  14000  dvdsdivcl  16398  isprm5  16790  latjlej1  18533  latmlem1  18549  chnccat  18706  cnrest2  23495  cnpresti  23497  trufil  24120  stdbdxmet  24725  lgsdir  27549  elwwlks2  30387  orthin  31871  mdbr2  32721  dmdbr2  32728  mdsl2i  32747  atcvat4i  32822  mdsymlem3  32830  fnfvintima  35537  tz9.1regs  35606  wzel  36353  ontgval  37001  poimirlem3  38333  poimirlem4  38334  poimirlem29  38359  poimir  38363  suceldisj  39527  cmtbr4N  40089  cvrat4  40277  cdlemblem  40627  negexpidd  43473  3cubeslem1  43475  tfsconcatb0  44131  ensucne0OLD  44316  itschlc0xyqsol  49606  elpglem2  50549