Theorem jcai 506

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

Syntax hints:   → wi 4   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  euan  2679  reu6  3547  f1ocnv2d  7037  onfin2  8312  nnoddn2prm  15723  isinitoi  16860  istermoi  16861  iszeroi  16866  mpfrcl  19733  cpmatelimp  20737  cpmatelimp2  20739  clwlksf1clwwlklemOLD  27249  f1o3d  29771  oddpwdc  30756  altopthsn  32405  volsupnfl  33786  mbfresfi  33787  qirropth  37997  brcofffn  38853  lighneal  42051