Theorem jctird 535

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 26	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 521	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anc2ri  565  pm5.31  843  fnun  6649  fcof  6729  brinxper  8720  mapdom2  9132  fisupg  9244  fiint  9282  dffi3  9387  fiinfg  9457  dfac2b  10110  nnadju  10177  cflm  10228  cfslbn  10246  cardmin  10543  fpwwe2lem11  10621  fpwwe2lem12  10622  elfznelfzob  13799  modsumfzodifsn  13976  dvdsdivcl  16369  isprm5  16761  latjlej1  18504  latmlem1  18520  chnccat  18677  cnrest2  23443  cnpresti  23445  trufil  24067  stdbdxmet  24672  lgsdir  27496  elwwlks2  30318  orthin  31798  mdbr2  32648  dmdbr2  32655  mdsl2i  32674  atcvat4i  32749  mdsymlem3  32757  fnfvintima  35476  tz9.1regs  35547  wzel  36314  ontgval  36942  poimirlem3  38274  poimirlem4  38275  poimirlem29  38300  poimir  38304  suceldisj  39467  cmtbr4N  40029  cvrat4  40217  cdlemblem  40567  negexpidd  43413  3cubeslem1  43415  tfsconcatb0  44071  ensucne0OLD  44256  itschlc0xyqsol  49547  elpglem2  50490