Theorem jcai 526

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  euan  2646  euanv  2649  reu6  3683  f1ocnv2d  7674  onfin2  9235  nnoddn2prm  16994  isinitoi  18179  istermoi  18180  iszeroi  18189  mpfrcl  22399  cpmatelimp  23035  cpmatelimp2  23037  f1o3d  33267  oddpwdc  35032  reu6f  35755  altopthsn  36818  bj-animbi  37520  volsupnfl  38676  mbfresfi  38677  qirropth  44008  oacl2g  44425  omabs2  44427  omcl2  44428  ofoafg  44449  ofoafo  44451  naddcnff  44457  naddcnffo  44459  brcofffn  45124  lighneal  48789