Theorem jctird 526

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anc2ri  556  pm5.31  830  fnun  6662  fcof  6739  brinxper  8756  mapdom2  9170  fisupg  9306  fiint  9348  fiintOLD  9349  dffi3  9453  fiinfg  9521  dfac2b  10153  nnadju  10220  cflm  10272  cfslbn  10289  cardmin  10586  fpwwe2lem11  10663  fpwwe2lem12  10664  elfznelfzob  13794  modsumfzodifsn  13967  dvdsdivcl  16335  isprm5  16726  latjlej1  18467  latmlem1  18483  cnrest2  23240  cnpresti  23242  trufil  23864  stdbdxmet  24472  lgsdir  27312  elwwlks2  29914  orthin  31393  mdbr2  32243  dmdbr2  32250  mdsl2i  32269  atcvat4i  32344  mdsymlem3  32352  wzel  35784  ontgval  36391  poimirlem3  37589  poimirlem4  37590  poimirlem29  37615  poimir  37619  cmtbr4N  39215  cvrat4  39404  cdlemblem  39754  negexpidd  42656  3cubeslem1  42658  tfsconcatb0  43319  ensucne0OLD  43505  itschlc0xyqsol  48646  elpglem2  49239