MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimp3a 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  10222  nn0addge2  10223  nn0sub2  10291  eluzp1p1  10467  uznn0sub  10473  iocssre  10946  icossre  10947  iccssre  10948  lincmb01cmp  10994  iccf1o  10995  hashprb  11623  eflt  12673  prmdiv  13129  coprimeprodsq  13138  pythagtrip  13163  spwcl  14617  odinf  15154  odcl2  15156  tgtop11  17002  restntr  17200  hauscmplem  17423  icchmeo  18919  pi1xfr  19033  sinq12gt0  20368  tanord1  20392  ghomlin  21905  ghomid  21906  nv1  22118  lnolin  22208  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemrv2  24732  ghomfo  25055  ghomgsg  25057  br8  25327  br6  25328  br4  25329  axsegconlem6  25765  ismtyima  26402  ismtybndlem  26405  jm2.17b  26916  hashgcdlem  27384  bi123impia  28286  cvrcmp2  29767  atcvrj2  29915  1cvratex  29955  lplnric  30034  lplnri1  30035  lnatexN  30261  ltrnateq  30663  ltrnatneq  30664  cdleme46f2g2  30975  cdleme46f2g1  30976  dibelval1st  31632  dibelval2nd  31635  dicelval1sta  31670  hlhilphllem  32445
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