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  2616  euanv  2619  reu6  3680  f1ocnv2d  7599  onfin2  9125  nnoddn2prm  16723  isinitoi  17906  istermoi  17907  iszeroi  17916  mpfrcl  22020  cpmatelimp  22627  cpmatelimp2  22629  f1o3d  32608  oddpwdc  34367  altopthsn  36005  bj-animbi  36603  volsupnfl  37704  mbfresfi  37705  qirropth  43000  oacl2g  43422  omabs2  43424  omcl2  43425  ofoafg  43446  ofoafo  43448  naddcnff  43454  naddcnffo  43456  brcofffn  44123  lighneal  47710