Theorem jctird 527

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  anc2ri  557  pm5.31  828  fnun  6538  fcof  6616  fcoOLD  6618  mapdom2  8923  fisupg  9050  fiint  9079  dffi3  9178  fiinfg  9246  dfac2b  9874  nnadju  9941  cflm  9994  cfslbn  10011  cardmin  10308  fpwwe2lem11  10385  fpwwe2lem12  10386  elfznelfzob  13481  modsumfzodifsn  13652  dvdsdivcl  16013  isprm5  16400  latjlej1  18159  latmlem1  18175  cnrest2  22425  cnpresti  22427  trufil  23049  stdbdxmet  23659  lgsdir  26468  elwwlks2  28317  orthin  29794  mdbr2  30644  dmdbr2  30651  mdsl2i  30670  atcvat4i  30745  mdsymlem3  30753  wzel  33804  ontgval  34606  poimirlem3  35766  poimirlem4  35767  poimirlem29  35792  poimir  35796  cmtbr4N  37255  cvrat4  37443  cdlemblem  37793  negexpidd  40490  3cubeslem1  40492  ensucne0OLD  41105  itschlc0xyqsol  46069  elpglem2  46373