Theorem jctird 526

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anc2ri  556  pm5.31  831  fnun  6607  fcof  6686  brinxper  8667  mapdom2  9080  fisupg  9192  fiint  9231  dffi3  9338  fiinfg  9408  dfac2b  10045  nnadju  10112  cflm  10164  cfslbn  10181  cardmin  10478  fpwwe2lem11  10556  fpwwe2lem12  10557  elfznelfzob  13694  modsumfzodifsn  13871  dvdsdivcl  16247  isprm5  16638  latjlej1  18380  latmlem1  18396  chnccat  18553  cnrest2  23234  cnpresti  23236  trufil  23858  stdbdxmet  24463  lgsdir  27303  elwwlks2  30025  orthin  31504  mdbr2  32354  dmdbr2  32361  mdsl2i  32380  atcvat4i  32455  mdsymlem3  32463  tz9.1regs  35271  wzel  35997  ontgval  36606  poimirlem3  37795  poimirlem4  37796  poimirlem29  37821  poimir  37825  suceldisj  38990  cmtbr4N  39552  cvrat4  39740  cdlemblem  40090  negexpidd  42960  3cubeslem1  42962  tfsconcatb0  43622  ensucne0OLD  43807  itschlc0xyqsol  49049  elpglem2  49993