Theorem jcai 516

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  euan  2621  euanv  2624  reu6  3672  f1ocnv2d  7620  onfin2  9151  nnoddn2prm  16782  isinitoi  17966  istermoi  17967  iszeroi  17976  mpfrcl  22063  cpmatelimp  22677  cpmatelimp2  22679  f1o3d  32699  oddpwdc  34498  altopthsn  36143  bj-animbi  36823  volsupnfl  37986  mbfresfi  37987  qirropth  43336  oacl2g  43758  omabs2  43760  omcl2  43761  ofoafg  43782  ofoafo  43784  naddcnff  43790  naddcnffo  43792  brcofffn  44458  lighneal  48074