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  6545  fcof  6623  fcoOLD  6625  mapdom2  8935  fisupg  9062  fiint  9091  dffi3  9190  fiinfg  9258  dfac2b  9886  nnadju  9953  cflm  10006  cfslbn  10023  cardmin  10320  fpwwe2lem11  10397  fpwwe2lem12  10398  elfznelfzob  13493  modsumfzodifsn  13664  dvdsdivcl  16025  isprm5  16412  latjlej1  18171  latmlem1  18187  cnrest2  22437  cnpresti  22439  trufil  23061  stdbdxmet  23671  lgsdir  26480  elwwlks2  28331  orthin  29808  mdbr2  30658  dmdbr2  30665  mdsl2i  30684  atcvat4i  30759  mdsymlem3  30767  wzel  33818  ontgval  34620  poimirlem3  35780  poimirlem4  35781  poimirlem29  35806  poimir  35810  cmtbr4N  37269  cvrat4  37457  cdlemblem  37807  negexpidd  40504  3cubeslem1  40506  ensucne0OLD  41137  itschlc0xyqsol  46113  elpglem2  46417