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  2615  euanv  2618  reu6  3700  f1ocnv2d  7645  onfin2  9186  nnoddn2prm  16789  isinitoi  17968  istermoi  17969  iszeroi  17978  mpfrcl  21999  cpmatelimp  22606  cpmatelimp2  22608  f1o3d  32558  oddpwdc  34352  altopthsn  35956  bj-animbi  36554  volsupnfl  37666  mbfresfi  37667  qirropth  42903  oacl2g  43326  omabs2  43328  omcl2  43329  ofoafg  43350  ofoafo  43352  naddcnff  43358  naddcnffo  43360  brcofffn  44027  lighneal  47616