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  2621  euanv  2624  reu6  3732  f1ocnv2d  7686  onfin2  9268  nnoddn2prm  16849  isinitoi  18044  istermoi  18045  iszeroi  18054  mpfrcl  22109  cpmatelimp  22718  cpmatelimp2  22720  f1o3d  32637  oddpwdc  34356  altopthsn  35962  bj-animbi  36560  volsupnfl  37672  mbfresfi  37673  qirropth  42919  oacl2g  43343  omabs2  43345  omcl2  43346  ofoafg  43367  ofoafo  43369  naddcnff  43375  naddcnffo  43377  brcofffn  44044  lighneal  47598