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  2620  euanv  2623  reu6  3709  f1ocnv2d  7660  onfin2  9240  nnoddn2prm  16831  isinitoi  18012  istermoi  18013  iszeroi  18022  mpfrcl  22043  cpmatelimp  22650  cpmatelimp2  22652  f1o3d  32605  oddpwdc  34386  altopthsn  35979  bj-animbi  36577  volsupnfl  37689  mbfresfi  37690  qirropth  42931  oacl2g  43354  omabs2  43356  omcl2  43357  ofoafg  43378  ofoafo  43380  naddcnff  43386  naddcnffo  43388  brcofffn  44055  lighneal  47625