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  2652  euanv  2655  reu6  3692  f1ocnv2d  7676  onfin2  9211  nnoddn2prm  16896  isinitoi  18081  istermoi  18082  iszeroi  18091  mpfrcl  22273  cpmatelimp  22906  cpmatelimp2  22908  f1o3d  33008  oddpwdc  34776  altopthsn  36474  bj-animbi  37192  volsupnfl  38357  mbfresfi  38358  qirropth  43676  oacl2g  44098  omabs2  44100  omcl2  44101  ofoafg  44122  ofoafo  44124  naddcnff  44130  naddcnffo  44132  brcofffn  44798  lighneal  48404