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

This theorem is referenced by:  euan  2624  euanv  2627  reu6  3664  f1ocnv2d  7513  onfin2  8977  nnoddn2prm  16493  isinitoi  17695  istermoi  17696  iszeroi  17705  mpfrcl  21276  cpmatelimp  21842  cpmatelimp2  21844  f1o3d  30941  oddpwdc  32300  altopthsn  34242  bj-animbi  34718  volsupnfl  35801  mbfresfi  35802  qirropth  40710  brcofffn  41594  lighneal  45015