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  830  fnun  6635  fcof  6714  brinxper  8703  mapdom2  9118  fisupg  9242  fiint  9284  fiintOLD  9285  dffi3  9389  fiinfg  9459  dfac2b  10091  nnadju  10158  cflm  10210  cfslbn  10227  cardmin  10524  fpwwe2lem11  10601  fpwwe2lem12  10602  elfznelfzob  13741  modsumfzodifsn  13916  dvdsdivcl  16293  isprm5  16684  latjlej1  18419  latmlem1  18435  cnrest2  23180  cnpresti  23182  trufil  23804  stdbdxmet  24410  lgsdir  27250  elwwlks2  29903  orthin  31382  mdbr2  32232  dmdbr2  32239  mdsl2i  32258  atcvat4i  32333  mdsymlem3  32341  wzel  35819  ontgval  36426  poimirlem3  37624  poimirlem4  37625  poimirlem29  37650  poimir  37654  cmtbr4N  39255  cvrat4  39444  cdlemblem  39794  negexpidd  42677  3cubeslem1  42679  tfsconcatb0  43340  ensucne0OLD  43526  itschlc0xyqsol  48760  elpglem2  49705