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  6607  fcof  6686  brinxper  8667  mapdom2  9080  fisupg  9192  fiint  9231  dffi3  9338  fiinfg  9408  dfac2b  10047  nnadju  10114  cflm  10166  cfslbn  10183  cardmin  10480  fpwwe2lem11  10558  fpwwe2lem12  10559  elfznelfzob  13723  modsumfzodifsn  13900  dvdsdivcl  16279  isprm5  16671  latjlej1  18413  latmlem1  18429  chnccat  18586  cnrest2  23264  cnpresti  23266  trufil  23888  stdbdxmet  24493  lgsdir  27312  elwwlks2  30055  orthin  31535  mdbr2  32385  dmdbr2  32392  mdsl2i  32411  atcvat4i  32486  mdsymlem3  32494  tz9.1regs  35297  wzel  36023  ontgval  36632  poimirlem3  37961  poimirlem4  37962  poimirlem29  37987  poimir  37991  suceldisj  39156  cmtbr4N  39718  cvrat4  39906  cdlemblem  40256  negexpidd  43131  3cubeslem1  43133  tfsconcatb0  43793  ensucne0OLD  43978  itschlc0xyqsol  49258  elpglem2  50202