Theorem jcai 521

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

Syntax hints:   → wi 4   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  euan  2625  euanv  2628  reu6  3674  f1ocnv2d  7616  onfin2  9148  nnoddn2prm  16780  isinitoi  17964  istermoi  17965  iszeroi  17974  mpfrcl  22068  cpmatelimp  22702  cpmatelimp2  22704  f1o3d  32725  oddpwdc  34545  altopthsn  36196  bj-animbi  36876  volsupnfl  38039  mbfresfi  38040  qirropth  43360  oacl2g  43782  omabs2  43784  omcl2  43785  ofoafg  43806  ofoafo  43808  naddcnff  43814  naddcnffo  43816  brcofffn  44482  lighneal  48096