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  2646  euanv  2649  reu6  3683  f1ocnv2d  7674  onfin2  9232  nnoddn2prm  16989  isinitoi  18174  istermoi  18175  iszeroi  18184  mpfrcl  22394  cpmatelimp  23030  cpmatelimp2  23032  f1o3d  33262  oddpwdc  35028  altopthsn  36768  bj-animbi  37470  volsupnfl  38626  mbfresfi  38627  qirropth  43957  oacl2g  44374  omabs2  44376  omcl2  44377  ofoafg  44398  ofoafo  44400  naddcnff  44406  naddcnffo  44408  brcofffn  45073  lighneal  48738