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  2614  euanv  2617  reu6  3697  f1ocnv2d  7642  onfin2  9180  nnoddn2prm  16782  isinitoi  17961  istermoi  17962  iszeroi  17971  mpfrcl  21992  cpmatelimp  22599  cpmatelimp2  22601  f1o3d  32551  oddpwdc  34345  altopthsn  35949  bj-animbi  36547  volsupnfl  37659  mbfresfi  37660  qirropth  42896  oacl2g  43319  omabs2  43321  omcl2  43322  ofoafg  43343  ofoafo  43345  naddcnff  43351  naddcnffo  43353  brcofffn  44020  lighneal  47612