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  3720  f1ocnv2d  7646  onfin2  9219  nnoddn2prm  16731  isinitoi  17936  istermoi  17937  iszeroi  17946  mpfrcl  21617  cpmatelimp  22183  cpmatelimp2  22185  f1o3d  31820  oddpwdc  33284  altopthsn  34864  bj-animbi  35340  volsupnfl  36438  mbfresfi  36439  qirropth  41517  oacl2g  41951  omabs2  41953  omcl2  41954  ofoafg  41975  ofoafo  41977  naddcnff  41983  naddcnffo  41985  brcofffn  42653  lighneal  46152