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  2648  euanv  2651  reu6  3687  f1ocnv2d  7671  onfin2  9215  nnoddn2prm  16909  isinitoi  18094  istermoi  18095  iszeroi  18104  mpfrcl  22307  cpmatelimp  22943  cpmatelimp2  22945  f1o3d  33107  oddpwdc  34873  altopthsn  36549  bj-animbi  37267  volsupnfl  38422  mbfresfi  38423  qirropth  43757  oacl2g  44179  omabs2  44181  omcl2  44182  ofoafg  44203  ofoafo  44205  naddcnff  44211  naddcnffo  44213  brcofffn  44879  lighneal  48522