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  2649  euanv  2652  reu6  3690  f1ocnv2d  7665  onfin2  9202  nnoddn2prm  16872  isinitoi  18057  istermoi  18058  iszeroi  18067  mpfrcl  22217  cpmatelimp  22850  cpmatelimp2  22852  f1o3d  32949  oddpwdc  34722  altopthsn  36431  bj-animbi  37129  volsupnfl  38294  mbfresfi  38295  qirropth  43615  oacl2g  44037  omabs2  44039  omcl2  44040  ofoafg  44061  ofoafo  44063  naddcnff  44069  naddcnffo  44071  brcofffn  44737  lighneal  48340