Theorem jcai 517

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 512	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 206  df-an 397

This theorem is referenced by:  euan  2617  euanv  2620  reu6  3719  f1ocnv2d  7643  onfin2  9216  nnoddn2prm  16728  isinitoi  17933  istermoi  17934  iszeroi  17943  mpfrcl  21579  cpmatelimp  22145  cpmatelimp2  22147  f1o3d  31783  oddpwdc  33248  altopthsn  34827  bj-animbi  35303  volsupnfl  36401  mbfresfi  36402  qirropth  41481  oacl2g  41915  omabs2  41917  omcl2  41918  ofoafg  41939  ofoafo  41941  naddcnff  41947  naddcnffo  41949  brcofffn  42617  lighneal  46115