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  2705  euanv  2708  reu6  3720  f1ocnv2d  7401  onfin2  8713  nnoddn2prm  16151  isinitoi  17266  istermoi  17267  iszeroi  17272  mpfrcl  20301  cpmatelimp  21323  cpmatelimp2  21325  f1o3d  30375  oddpwdc  31616  altopthsn  33426  bj-animbi  33898  volsupnfl  34941  mbfresfi  34942  qirropth  39511  brcofffn  40387  lighneal  43783