Theorem jctird 535

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 521	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anc2ri  565  pm5.31  843  fnun  6650  fcof  6730  brinxper  8723  mapdom2  9135  fisupg  9247  fiint  9285  dffi3  9390  fiinfg  9460  dfac2b  10113  nnadju  10180  cflm  10232  cfslbn  10250  cardmin  10547  fpwwe2lem11  10625  fpwwe2lem12  10626  elfznelfzob  13802  modsumfzodifsn  13979  dvdsdivcl  16373  isprm5  16765  latjlej1  18508  latmlem1  18524  chnccat  18681  cnrest2  23411  cnpresti  23413  trufil  24035  stdbdxmet  24640  lgsdir  27461  elwwlks2  30258  orthin  31738  mdbr2  32588  dmdbr2  32595  mdsl2i  32614  atcvat4i  32689  mdsymlem3  32697  tz9.1regs  35469  wzel  36212  ontgval  36830  poimirlem3  38161  poimirlem4  38162  poimirlem29  38187  poimir  38191  suceldisj  39356  cmtbr4N  39918  cvrat4  40106  cdlemblem  40456  negexpidd  43304  3cubeslem1  43306  tfsconcatb0  43962  ensucne0OLD  44147  itschlc0xyqsol  49431  elpglem2  50374