Theorem jcai 557

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  euan  2518  reu6  3362  f1ocnv2d  6784  onfin2  8037  nnoddn2prm  15354  isinitoi  16476  istermoi  16477  iszeroi  16482  mpfrcl  19339  cpmatelimp  20336  cpmatelimp2  20338  clwlkf1clwwlklem  26376  f1o3d  28813  oddpwdc  29743  altopthsn  31238  volsupnfl  32624  mbfresfi  32626  qirropth  36491  brcofffn  37349  lighneal  40066  clwlksf1clwwlklem  41275