Theorem jctird 565

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anc2ri  579  fnun  5911  fco  5971  mapdom2  8016  fisupg  8093  fiint  8122  dffi3  8220  fiinfg  8288  dfac2  8836  cflm  8955  cfslbn  8972  cardmin  9265  fpwwe2lem12  9342  fpwwe2lem13  9343  elfznelfzob  12440  modsumfzodifsn  12605  dvdsdivcl  14876  isprm5  15257  latjlej1  16888  latmlem1  16904  cnrest2  20900  cnpresti  20902  trufil  21524  stdbdxmet  22130  lgsdir  24857  usgraedg4  25916  wlkdvspth  26138  el2spthonot  26397  orthin  27689  mdbr2  28539  dmdbr2  28546  mdsl2i  28565  atcvat4i  28640  mdsymlem3  28648  wzel  31015  wzelOLD  31016  ontgval  31600  bj-xnex  32245  poimirlem3  32582  poimirlem4  32583  poimirlem29  32608  poimir  32612  cmtbr4N  33560  cvrat4  33747  cdlemblem  34097  elwwlks2  41170  elpglem2  42254