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  2622  euanv  2625  reu6  3673  f1ocnv2d  7613  onfin2  9144  nnoddn2prm  16773  isinitoi  17957  istermoi  17958  iszeroi  17967  mpfrcl  22073  cpmatelimp  22687  cpmatelimp2  22689  f1o3d  32714  oddpwdc  34514  altopthsn  36159  bj-animbi  36839  volsupnfl  38000  mbfresfi  38001  qirropth  43354  oacl2g  43776  omabs2  43778  omcl2  43779  ofoafg  43800  ofoafo  43802  naddcnff  43808  naddcnffo  43810  brcofffn  44476  lighneal  48086