Theorem jctird 525

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  anc2ri  555  pm5.31  829  fnun  6669  fcof  6746  fcoOLD  6748  mapdom2  9173  fisupg  9316  fiint  9350  dffi3  9456  fiinfg  9524  dfac2b  10155  nnadju  10222  cflm  10275  cfslbn  10292  cardmin  10589  fpwwe2lem11  10666  fpwwe2lem12  10667  elfznelfzob  13774  modsumfzodifsn  13945  dvdsdivcl  16296  isprm5  16681  latjlej1  18448  latmlem1  18464  cnrest2  23234  cnpresti  23236  trufil  23858  stdbdxmet  24468  lgsdir  27310  elwwlks2  29849  orthin  31328  mdbr2  32178  dmdbr2  32185  mdsl2i  32204  atcvat4i  32279  mdsymlem3  32287  wzel  35551  ontgval  36046  poimirlem3  37227  poimirlem4  37228  poimirlem29  37253  poimir  37257  cmtbr4N  38857  cvrat4  39046  cdlemblem  39396  negexpidd  42244  3cubeslem1  42246  tfsconcatb0  42915  ensucne0OLD  43102  gricer  47376  itschlc0xyqsol  48026  elpglem2  48329