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  831  fnun  6614  fcof  6693  brinxper  8675  mapdom2  9088  fisupg  9200  fiint  9239  dffi3  9346  fiinfg  9416  dfac2b  10053  nnadju  10120  cflm  10172  cfslbn  10189  cardmin  10486  fpwwe2lem11  10564  fpwwe2lem12  10565  elfznelfzob  13702  modsumfzodifsn  13879  dvdsdivcl  16255  isprm5  16646  latjlej1  18388  latmlem1  18404  chnccat  18561  cnrest2  23242  cnpresti  23244  trufil  23866  stdbdxmet  24471  lgsdir  27311  elwwlks2  30054  orthin  31534  mdbr2  32384  dmdbr2  32391  mdsl2i  32410  atcvat4i  32485  mdsymlem3  32493  tz9.1regs  35312  wzel  36038  ontgval  36647  poimirlem3  37874  poimirlem4  37875  poimirlem29  37900  poimir  37904  suceldisj  39069  cmtbr4N  39631  cvrat4  39819  cdlemblem  40169  negexpidd  43039  3cubeslem1  43041  tfsconcatb0  43701  ensucne0OLD  43886  itschlc0xyqsol  49127  elpglem2  50071