Theorem jctird 530

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  anc2ri  560  pm5.31  829  fnun  6434  fco  6505  mapdom2  8672  fisupg  8750  fiint  8779  dffi3  8879  fiinfg  8947  dfac2b  9541  nnadju  9608  cflm  9661  cfslbn  9678  cardmin  9975  fpwwe2lem12  10052  fpwwe2lem13  10053  elfznelfzob  13138  modsumfzodifsn  13307  dvdsdivcl  15658  isprm5  16041  latjlej1  17667  latmlem1  17683  cnrest2  21891  cnpresti  21893  trufil  22515  stdbdxmet  23122  lgsdir  25916  elwwlks2  27752  orthin  29229  mdbr2  30079  dmdbr2  30086  mdsl2i  30105  atcvat4i  30180  mdsymlem3  30188  wzel  33224  ontgval  33892  poimirlem3  35060  poimirlem4  35061  poimirlem29  35086  poimir  35090  cmtbr4N  36551  cvrat4  36739  cdlemblem  37089  negexpidd  39623  3cubeslem1  39625  ensucne0OLD  40238  itschlc0xyqsol  45181  elpglem2  45241