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  6614  fcof  6693  brinxper  8677  mapdom2  9089  fisupg  9211  fiint  9253  fiintOLD  9254  dffi3  9358  fiinfg  9428  dfac2b  10060  nnadju  10127  cflm  10179  cfslbn  10196  cardmin  10493  fpwwe2lem11  10570  fpwwe2lem12  10571  elfznelfzob  13710  modsumfzodifsn  13885  dvdsdivcl  16262  isprm5  16653  latjlej1  18388  latmlem1  18404  cnrest2  23149  cnpresti  23151  trufil  23773  stdbdxmet  24379  lgsdir  27219  elwwlks2  29869  orthin  31348  mdbr2  32198  dmdbr2  32205  mdsl2i  32224  atcvat4i  32299  mdsymlem3  32307  wzel  35785  ontgval  36392  poimirlem3  37590  poimirlem4  37591  poimirlem29  37616  poimir  37620  cmtbr4N  39221  cvrat4  39410  cdlemblem  39760  negexpidd  42643  3cubeslem1  42645  tfsconcatb0  43306  ensucne0OLD  43492  itschlc0xyqsol  48729  elpglem2  49674