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  2618  euanv  2621  reu6  3681  f1ocnv2d  7605  onfin2  9132  nnoddn2prm  16725  isinitoi  17908  istermoi  17909  iszeroi  17918  mpfrcl  22021  cpmatelimp  22628  cpmatelimp2  22630  f1o3d  32610  oddpwdc  34388  altopthsn  36026  bj-animbi  36624  volsupnfl  37725  mbfresfi  37726  qirropth  43025  oacl2g  43447  omabs2  43449  omcl2  43450  ofoafg  43471  ofoafo  43473  naddcnff  43479  naddcnffo  43481  brcofffn  44148  lighneal  47735