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  10026  nn0addge2  10027  nn0sub2  10093  eluzp1p1  10269  uznn0sub  10275  iocssre  10745  icossre  10746  iccssre  10747  lincmb01cmp  10793  iccf1o  10794  eflt  12413  prmdiv  12869  coprimeprodsq  12878  pythagtrip  12903  spwcl  14355  odinf  14892  odcl2  14894  tgtop11  16736  restntr  16928  hauscmplem  17149  icchmeo  18455  pi1xfr  18569  sinq12gt0  19891  tanord1  19915  ghomlin  21047  ghomid  21048  nv1  21258  lnolin  21348  ballotlemrv2  23096  ghomfo  24013  ghomgsg  24015  br8  24184  br6  24185  br4  24186  axsegconlem6  24622  intcont  25646  prdnei  25676  islimrs4  25685  lvsovso  25729  fnctartar3  26012  rocatval  26062  pdiveql  26271  ismtyima  26630  ismtybndlem  26633  jm2.17b  27151  hashgcdlem  27619  cvrcmp2  30096  atcvrj2  30244  1cvratex  30284  lplnric  30363  lplnri1  30364  lnatexN  30590  ltrnateq  30992  ltrnatneq  30993  cdleme46f2g2  31304  cdleme46f2g1  31305  dibelval1st  31961  dibelval2nd  31964  dicelval1sta  31999  hlhilphllem  32774
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