Theorem jctird 516

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

Syntax hints:   → wi 4   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  anc2ri  546  fnun  6137  fco  6198  mapdom2  8287  fisupg  8364  fiint  8393  dffi3  8493  fiinfg  8561  dfac2b  9153  dfac2OLD  9155  cflm  9274  cfslbn  9291  cardmin  9588  fpwwe2lem12  9665  fpwwe2lem13  9666  elfznelfzob  12782  modsumfzodifsn  12951  dvdsdivcl  15247  isprm5  15626  latjlej1  17273  latmlem1  17289  cnrest2  21311  cnpresti  21313  trufil  21934  stdbdxmet  22540  lgsdir  25278  elwwlks2  27115  orthin  28645  mdbr2  29495  dmdbr2  29502  mdsl2i  29521  atcvat4i  29596  mdsymlem3  29604  wzel  32106  ontgval  32767  poimirlem3  33745  poimirlem4  33746  poimirlem29  33771  poimir  33775  cmtbr4N  35064  cvrat4  35251  cdlemblem  35601  elpglem2  42986