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 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  anc2ri  565  pm5.31  843  fnun  6649  fcof  6729  brinxper  8722  mapdom2  9134  fisupg  9246  fiint  9284  dffi3  9389  fiinfg  9459  dfac2b  10121  nnadju  10188  cflm  10239  cfslbn  10257  cardmin  10554  fpwwe2lem11  10632  fpwwe2lem12  10633  elfznelfzob  13810  modsumfzodifsn  13987  dvdsdivcl  16380  isprm5  16772  latjlej1  18515  latmlem1  18531  chnccat  18688  cnrest2  23454  cnpresti  23456  trufil  24078  stdbdxmet  24683  lgsdir  27507  elwwlks2  30329  orthin  31809  mdbr2  32659  dmdbr2  32666  mdsl2i  32685  atcvat4i  32760  mdsymlem3  32768  fnfvintima  35485  tz9.1regs  35555  wzel  36322  ontgval  36970  poimirlem3  38302  poimirlem4  38303  poimirlem29  38328  poimir  38332  suceldisj  39495  cmtbr4N  40057  cvrat4  40245  cdlemblem  40595  negexpidd  43441  3cubeslem1  43443  tfsconcatb0  44099  ensucne0OLD  44284  itschlc0xyqsol  49575  elpglem2  50518