Theorem jcai 519

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 514	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:  euan  2706  euanv  2709  reu6  3719  f1ocnv2d  7400  onfin2  8712  nnoddn2prm  16150  isinitoi  17265  istermoi  17266  iszeroi  17271  mpfrcl  20300  cpmatelimp  21322  cpmatelimp2  21324  f1o3d  30374  oddpwdc  31614  altopthsn  33424  bj-animbi  33896  volsupnfl  34939  mbfresfi  34940  qirropth  39512  brcofffn  40388  lighneal  43783