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  6606  fcof  6685  brinxper  8664  mapdom2  9076  fisupg  9188  fiint  9227  dffi3  9334  fiinfg  9404  dfac2b  10041  nnadju  10108  cflm  10160  cfslbn  10177  cardmin  10474  fpwwe2lem11  10552  fpwwe2lem12  10553  elfznelfzob  13690  modsumfzodifsn  13867  dvdsdivcl  16243  isprm5  16634  latjlej1  18376  latmlem1  18392  chnccat  18549  cnrest2  23230  cnpresti  23232  trufil  23854  stdbdxmet  24459  lgsdir  27299  elwwlks2  30042  orthin  31521  mdbr2  32371  dmdbr2  32378  mdsl2i  32397  atcvat4i  32472  mdsymlem3  32480  tz9.1regs  35290  wzel  36016  ontgval  36625  poimirlem3  37824  poimirlem4  37825  poimirlem29  37850  poimir  37854  cmtbr4N  39515  cvrat4  39703  cdlemblem  40053  negexpidd  42924  3cubeslem1  42926  tfsconcatb0  43586  ensucne0OLD  43771  itschlc0xyqsol  49013  elpglem2  49957