Theorem jcai 518

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 513	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  euan  2618  euanv  2621  reu6  3723  f1ocnv2d  7659  onfin2  9231  nnoddn2prm  16744  isinitoi  17949  istermoi  17950  iszeroi  17959  mpfrcl  21648  cpmatelimp  22214  cpmatelimp2  22216  f1o3d  31851  oddpwdc  33353  altopthsn  34933  bj-animbi  35435  volsupnfl  36533  mbfresfi  36534  qirropth  41646  oacl2g  42080  omabs2  42082  omcl2  42083  ofoafg  42104  ofoafo  42106  naddcnff  42112  naddcnffo  42114  brcofffn  42782  lighneal  46279