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

Theorem biimp3a 1283
Description: Infer implication from a logical equivalence. Similar to biimpa 471. (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 471 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
323impa 1148 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936
This theorem is referenced by:  nn0addge1  10258  nn0addge2  10259  nn0sub2  10327  eluzp1p1  10503  uznn0sub  10509  iocssre  10982  icossre  10983  iccssre  10984  lincmb01cmp  11030  iccf1o  11031  hashprb  11660  eflt  12710  prmdiv  13166  coprimeprodsq  13175  pythagtrip  13200  spwcl  14654  odinf  15191  odcl2  15193  tgtop11  17039  restntr  17238  hauscmplem  17461  icchmeo  18958  pi1xfr  19072  sinq12gt0  20407  tanord1  20431  ghomlin  21944  ghomid  21945  nv1  22157  lnolin  22247  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemrv2  24771  ghomfo  25094  ghomgsg  25096  br8  25371  br6  25372  br4  25373  axsegconlem6  25853  ismtyima  26503  ismtybndlem  26506  jm2.17b  27017  hashgcdlem  27484  cshwidx0  28210  2cshw1lem3  28216  cshwssizelem4a  28246  bi123impia  28509  sineq0ALT  28986  cvrcmp2  30019  atcvrj2  30167  1cvratex  30207  lplnric  30286  lplnri1  30287  lnatexN  30513  ltrnateq  30915  ltrnatneq  30916  cdleme46f2g2  31227  cdleme46f2g1  31228  dibelval1st  31884  dibelval2nd  31887  dicelval1sta  31922  hlhilphllem  32697
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator