Theorem jcai 524

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  euan  2647  euanv  2650  reu6  3688  f1ocnv2d  7645  onfin2  9181  nnoddn2prm  16830  isinitoi  18015  istermoi  18016  iszeroi  18025  mpfrcl  22118  cpmatelimp  22752  cpmatelimp2  22754  f1o3d  32778  oddpwdc  34612  altopthsn  36275  bj-animbi  36965  volsupnfl  38128  mbfresfi  38129  qirropth  43449  oacl2g  43871  omabs2  43873  omcl2  43874  ofoafg  43895  ofoafo  43897  naddcnff  43903  naddcnffo  43905  brcofffn  44571  lighneal  48184