Theorem jcai 520

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  euan  2622  euanv  2625  reu6  3639  f1ocnv2d  7458  onfin2  8871  nnoddn2prm  16364  isinitoi  17505  istermoi  17506  iszeroi  17515  mpfrcl  21045  cpmatelimp  21609  cpmatelimp2  21611  f1o3d  30681  oddpwdc  32033  altopthsn  34000  bj-animbi  34476  volsupnfl  35559  mbfresfi  35560  qirropth  40433  brcofffn  41318  lighneal  44736