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

Theorem biimp3a 1328
Description: Infer implication from a logical equivalence. Similar to biimpa 484. (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 484 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
323impa 1191 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  nn0addge1  10843  nn0addge2  10844  nn0sub2  10924  eluzp1p1  11108  uznn0sub  11114  iocssre  11605  icossre  11606  iccssre  11607  lincmb01cmp  11664  iccf1o  11665  fzosplitprm1  11888  hashprb  12431  swrd0fv  12632  eflt  13716  prmdiv  14177  coprimeprodsq  14195  pythagtrip  14220  cshwshashlem2  14442  odinf  16400  odcl2  16402  slesolex  18991  tgtop11  19290  restntr  19489  hauscmplem  19712  icchmeo  21268  pi1xfr  21382  sinq12gt0  22725  tanord1  22749  axsegconlem6  23998  ghomlin  25139  ghomid  25140  nv1  25352  lnolin  25442  br8d  27233  ballotlemfc0  28182  ballotlemfcc  28183  ballotlemrv2  28211  ghomfo  28782  ghomgsg  28784  br8  29038  br6  29039  br4  29040  ismtyima  30129  ismtybndlem  30132  jm2.17b  30730  hashgcdlem  30989  ioomidp  31345  bi123impia  32554  sineq0ALT  33034  cvrcmp2  34298  atcvrj2  34446  1cvratex  34486  lplnric  34565  lplnri1  34566  lnatexN  34792  ltrnateq  35194  ltrnatneq  35195  cdleme46f2g2  35506  cdleme46f2g1  35507  dibelval1st  36163  dibelval2nd  36166  dicelval1sta  36201  hlhilphllem  36976
  Copyright terms: Public domain W3C validator