Theorem jctird 531

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 517	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 208  df-an 397

This theorem is referenced by:  anc2ri  561  pm5.31  836  fnun  6599  fcof  6678  brinxper  8663  mapdom2  9076  fisupg  9188  fiint  9227  dffi3  9334  fiinfg  9404  dfac2b  10044  nnadju  10111  cflm  10163  cfslbn  10180  cardmin  10477  fpwwe2lem11  10555  fpwwe2lem12  10556  elfznelfzob  13720  modsumfzodifsn  13897  dvdsdivcl  16276  isprm5  16668  latjlej1  18410  latmlem1  18426  chnccat  18583  cnrest2  23269  cnpresti  23271  trufil  23893  stdbdxmet  24498  lgsdir  27313  elwwlks2  30055  orthin  31535  mdbr2  32385  dmdbr2  32392  mdsl2i  32411  atcvat4i  32486  mdsymlem3  32494  tz9.1regs  35315  wzel  36050  ontgval  36659  poimirlem3  37990  poimirlem4  37991  poimirlem29  38016  poimir  38020  suceldisj  39185  cmtbr4N  39747  cvrat4  39935  cdlemblem  40285  negexpidd  43131  3cubeslem1  43133  tfsconcatb0  43789  ensucne0OLD  43974  itschlc0xyqsol  49258  elpglem2  50202