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

Theorem biimp3a 1281
Description: Infer implication from a logical equivalence. Similar to biimpa 470. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
biimp3a.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
biimp3a  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem biimp3a
StepHypRef Expression
1 biimp3a.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
21biimpa 470 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
323impa 1146 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934
This theorem is referenced by:  nn0addge1  10010  nn0addge2  10011  nn0sub2  10077  eluzp1p1  10253  uznn0sub  10259  iocssre  10729  icossre  10730  iccssre  10731  lincmb01cmp  10777  iccf1o  10778  eflt  12397  prmdiv  12853  coprimeprodsq  12862  pythagtrip  12887  spwcl  14339  odinf  14876  odcl2  14878  tgtop11  16720  restntr  16912  hauscmplem  17133  icchmeo  18439  pi1xfr  18553  sinq12gt0  19875  tanord1  19899  ghomlin  21031  ghomid  21032  nv1  21242  lnolin  21332  ballotlemrv2  23080  ghomfo  23998  ghomgsg  24000  br8  24113  br6  24114  br4  24115  axsegconlem6  24550  intcont  25543  prdnei  25573  islimrs4  25582  lvsovso  25626  fnctartar3  25909  rocatval  25959  pdiveql  26168  ismtyima  26527  ismtybndlem  26530  jm2.17b  27048  hashgcdlem  27516  cvrcmp2  29474  atcvrj2  29622  1cvratex  29662  lplnric  29741  lplnri1  29742  lnatexN  29968  ltrnateq  30370  ltrnatneq  30371  cdleme46f2g2  30682  cdleme46f2g1  30683  dibelval1st  31339  dibelval2nd  31342  dicelval1sta  31377  hlhilphllem  32152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator