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

Theorem jcai 534
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 530 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  euan  2348  reu6  3285  f1ocnv2d  6499  onfin2  7702  isinitoi  15481  istermoi  15482  iszeroi  15487  mpfrcl  18382  cpmatelimp  19380  cpmatelimp2  19382  clwlkf1clwwlklem  25051  f1o3d  27690  oddpwdc  28557  altopthsn  29839  volsupnfl  30299  mbfresfi  30301  qirropth  31083
  Copyright terms: Public domain W3C validator