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  2616  euanv  2619  reu6  3685  f1ocnv2d  7599  onfin2  9125  nnoddn2prm  16720  isinitoi  17903  istermoi  17904  iszeroi  17913  mpfrcl  22018  cpmatelimp  22625  cpmatelimp2  22627  f1o3d  32603  oddpwdc  34362  altopthsn  35994  bj-animbi  36592  volsupnfl  37704  mbfresfi  37705  qirropth  42940  oacl2g  43362  omabs2  43364  omcl2  43365  ofoafg  43386  ofoafo  43388  naddcnff  43394  naddcnffo  43396  brcofffn  44063  lighneal  47641