Theorem jcai 526

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 16	. 2 ⊢ (𝜑 → 𝜒)
4	1, 3	jca 521	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  euan  2647  euanv  2650  reu6  3684  f1ocnv2d  7666  onfin2  9216  nnoddn2prm  16969  isinitoi  18154  istermoi  18155  iszeroi  18164  mpfrcl  22374  cpmatelimp  23010  cpmatelimp2  23012  f1o3d  33202  oddpwdc  34969  altopthsn  36696  bj-animbi  37398  volsupnfl  38551  mbfresfi  38552  qirropth  43868  oacl2g  44290  omabs2  44292  omcl2  44293  ofoafg  44314  ofoafo  44316  naddcnff  44322  naddcnffo  44324  brcofffn  44990  lighneal  48640