Theorem jcai 520

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 515	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  euan  2683  euanv  2686  reu6  3665  f1ocnv2d  7378  onfin2  8695  nnoddn2prm  16138  isinitoi  17255  istermoi  17256  iszeroi  17261  mpfrcl  20757  cpmatelimp  21317  cpmatelimp2  21319  f1o3d  30386  oddpwdc  31722  altopthsn  33535  bj-animbi  34007  volsupnfl  35102  mbfresfi  35103  qirropth  39849  brcofffn  40734  lighneal  44129