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  6682  fcof  6759  brinxper  8772  mapdom2  9186  fisupg  9321  fiint  9363  fiintOLD  9364  dffi3  9468  fiinfg  9536  dfac2b  10168  nnadju  10235  cflm  10287  cfslbn  10304  cardmin  10601  fpwwe2lem11  10678  fpwwe2lem12  10679  elfznelfzob  13808  modsumfzodifsn  13981  dvdsdivcl  16349  isprm5  16740  latjlej1  18510  latmlem1  18526  cnrest2  23309  cnpresti  23311  trufil  23933  stdbdxmet  24543  lgsdir  27390  elwwlks2  29995  orthin  31474  mdbr2  32324  dmdbr2  32331  mdsl2i  32350  atcvat4i  32425  mdsymlem3  32433  wzel  35805  ontgval  36413  poimirlem3  37609  poimirlem4  37610  poimirlem29  37635  poimir  37639  cmtbr4N  39236  cvrat4  39425  cdlemblem  39775  negexpidd  42669  3cubeslem1  42671  tfsconcatb0  43333  ensucne0OLD  43519  itschlc0xyqsol  48616  elpglem2  48942