Theorem jctird 529

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anc2ri  559  pm5.31  828  fnun  6463  fco  6531  mapdom2  8688  fisupg  8766  fiint  8795  dffi3  8895  fiinfg  8963  dfac2b  9556  cflm  9672  cfslbn  9689  cardmin  9986  fpwwe2lem12  10063  fpwwe2lem13  10064  elfznelfzob  13144  modsumfzodifsn  13313  dvdsdivcl  15666  isprm5  16051  latjlej1  17675  latmlem1  17691  cnrest2  21894  cnpresti  21896  trufil  22518  stdbdxmet  23125  lgsdir  25908  elwwlks2  27745  orthin  29223  mdbr2  30073  dmdbr2  30080  mdsl2i  30099  atcvat4i  30174  mdsymlem3  30182  wzel  33111  ontgval  33779  poimirlem3  34910  poimirlem4  34911  poimirlem29  34936  poimir  34940  cmtbr4N  36406  cvrat4  36594  cdlemblem  36944  negexpidd  39299  3cubeslem1  39301  ensucne0OLD  39916  itschlc0xyqsol  44774  elpglem2  44834