MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jcai Structured version   Visualization version   Unicode version

Theorem jcai 543
Description: Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.)
Hypotheses
Ref Expression
jcai.1  |-  ( ph  ->  ps )
jcai.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
jcai  |-  ( ph  ->  ( ps  /\  ch ) )

Proof of Theorem jcai
StepHypRef Expression
1 jcai.1 . 2  |-  ( ph  ->  ps )
2 jcai.2 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2mpd 15 . 2  |-  ( ph  ->  ch )
41, 3jca 539 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  euan  2369  reu6  3238  f1ocnv2d  6546  onfin2  7789  isinitoi  15946  istermoi  15947  iszeroi  15952  mpfrcl  18789  cpmatelimp  19784  cpmatelimp2  19786  clwlkf1clwwlklem  25625  f1o3d  28277  oddpwdc  29235  altopthsn  30776  volsupnfl  32029  mbfresfi  32031  qirropth  35800
  Copyright terms: Public domain W3C validator