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  3684  f1ocnv2d  7611  onfin2  9141  nnoddn2prm  16739  isinitoi  17923  istermoi  17924  iszeroi  17933  mpfrcl  22040  cpmatelimp  22656  cpmatelimp2  22658  f1o3d  32704  oddpwdc  34511  altopthsn  36155  bj-animbi  36759  volsupnfl  37862  mbfresfi  37863  qirropth  43146  oacl2g  43568  omabs2  43570  omcl2  43571  ofoafg  43592  ofoafo  43594  naddcnff  43600  naddcnffo  43602  brcofffn  44268  lighneal  47853