Theorem jcai 518

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  euan  2621  euanv  2624  reu6  3666  f1ocnv2d  7554  onfin2  9052  nnoddn2prm  16557  isinitoi  17759  istermoi  17760  iszeroi  17769  mpfrcl  21340  cpmatelimp  21906  cpmatelimp2  21908  f1o3d  31007  oddpwdc  32366  altopthsn  34308  bj-animbi  34784  volsupnfl  35866  mbfresfi  35867  qirropth  40767  brcofffn  41679  lighneal  45121