Theorem jcai 525

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 16	. 2 ⊢ (𝜑 → 𝜒)
4	1, 3	jca 520	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  euan  2651  euanv  2654  reu6  3692  f1ocnv2d  7653  onfin2  9189  nnoddn2prm  16861  isinitoi  18046  istermoi  18047  iszeroi  18056  mpfrcl  22196  cpmatelimp  22830  cpmatelimp2  22832  f1o3d  32883  oddpwdc  34661  altopthsn  36324  bj-animbi  37013  volsupnfl  38176  mbfresfi  38177  qirropth  43497  oacl2g  43919  omabs2  43921  omcl2  43922  ofoafg  43943  ofoafo  43945  naddcnff  43951  naddcnffo  43953  brcofffn  44619  lighneal  48218