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  2649  euanv  2652  reu6  3687  f1ocnv2d  7698  onfin2  9260  nnoddn2prm  17018  isinitoi  18203  istermoi  18204  iszeroi  18213  mpfrcl  22424  cpmatelimp  23060  cpmatelimp2  23062  f1o3d  33292  oddpwdc  35056  reu6f  35779  altopthsn  36904  bj-animbi  37606  volsupnfl  38775  mbfresfi  38776  qirropth  44108  oacl2g  44524  omabs2  44526  omcl2  44527  ofoafg  44548  ofoafo  44550  naddcnff  44556  naddcnffo  44558  brcofffn  45223  lighneal  48901