Theorem jctird 536

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

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

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 402

This theorem is used by:  anc2ri  566  pm5.31  844  fnun  6658  fcof  6738  brinxper  8755  mapdom2  9175  fisupg  9287  fiint  9326  dffi3  9430  fiinfg  9500  dfac2b  10216  nnadju  10283  cflm  10334  cfslbn  10352  cardmin  10655  fpwwe2lem11  10733  fpwwe2lem12  10734  elfznelfzob  13916  modsumfzodifsn  14094  dvdsdivcl  16495  isprm5  16892  latjlej1  18636  latmlem1  18652  chnccat  18809  cnrest2  23613  cnpresti  23615  trufil  24238  stdbdxmet  24843  lgsdir  27668  elwwlks2  30567  orthin  32057  mdbr2  32907  dmdbr2  32914  mdsl2i  32933  atcvat4i  33008  mdsymlem3  33016  rmo6  35760  fnfvintima  35766  tz9.1regs  35870  j0ltaleph  35959  wzel  36710  ontgval  37343  poimirlem3  38678  poimirlem4  38679  poimirlem29  38704  poimir  38708  suceldisj  39887  cmtbr4N  40449  cvrat4  40637  cdlemblem  40987  negexpidd  43829  3cubeslem1  43831  tfsconcatb0  44483  ensucne0OLD  44668  itschlc0xyqsol  50015  elpglem2  51016