Theorem jcai 560

Description: Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.)

Hypotheses

Ref	Expression
jcai.1	⊢ (𝜑 → 𝜓)
jcai.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
jcai	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Proof of Theorem jcai

Step	Hyp	Ref	Expression
1		jcai.1	. 2 ⊢ (𝜑 → 𝜓)
2		jcai.2	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	mpd 15	. 2 ⊢ (𝜑 → 𝜒)
4	1, 3	jca 555	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 383

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 385

This theorem is referenced by:  euan  2660  reu6  3528  f1ocnv2d  7043  onfin2  8309  nnoddn2prm  15710  isinitoi  16846  istermoi  16847  iszeroi  16852  mpfrcl  19712  cpmatelimp  20711  cpmatelimp2  20713  clwlksf1clwwlklemOLD  27214  f1o3d  29732  oddpwdc  30717  altopthsn  32366  volsupnfl  33759  mbfresfi  33761  qirropth  37967  brcofffn  38823  lighneal  42030