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  2624  euanv  2627  reu6  3748  f1ocnv2d  7703  onfin2  9294  nnoddn2prm  16858  isinitoi  18066  istermoi  18067  iszeroi  18076  mpfrcl  22132  cpmatelimp  22739  cpmatelimp2  22741  f1o3d  32646  oddpwdc  34319  altopthsn  35925  bj-animbi  36525  volsupnfl  37625  mbfresfi  37626  qirropth  42864  oacl2g  43292  omabs2  43294  omcl2  43295  ofoafg  43316  ofoafo  43318  naddcnff  43324  naddcnffo  43326  brcofffn  43993  lighneal  47485