Theorem jcai 508

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

Syntax hints:   → wi 4   ∧ wa 384

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

This theorem is referenced by:  euan  2705  reu6  3604  f1ocnv2d  7126  onfin2  8401  nnoddn2prm  15753  isinitoi  16877  istermoi  16878  iszeroi  16883  mpfrcl  19746  cpmatelimp  20751  cpmatelimp2  20753  clwlksf1clwwlklemOLD  27265  f1o3d  29781  oddpwdc  30764  altopthsn  32411  volsupnfl  33786  mbfresfi  33787  qirropth  37992  brcofffn  38847  lighneal  42121