Theorem jcai 516

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  euan  2622  euanv  2625  reu6  3686  f1ocnv2d  7621  onfin2  9153  nnoddn2prm  16751  isinitoi  17935  istermoi  17936  iszeroi  17945  mpfrcl  22052  cpmatelimp  22668  cpmatelimp2  22670  f1o3d  32715  oddpwdc  34531  altopthsn  36174  bj-animbi  36780  volsupnfl  37910  mbfresfi  37911  qirropth  43259  oacl2g  43681  omabs2  43683  omcl2  43684  ofoafg  43705  ofoafo  43707  naddcnff  43713  naddcnffo  43715  brcofffn  44381  lighneal  47965