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

Theorem biimp3a 1368
Description: Infer implication from a logical equivalence. Similar to biimpa 487. (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 487 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
323impa 1202 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 984
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 189  df-an 373  df-3an 986
This theorem is referenced by:  nn0addge1  10913  nn0addge2  10914  nn0sub2  10994  eluzp1p1  11181  uznn0sub  11187  uzinfi  11235  iocssre  11711  icossre  11712  iccssre  11713  lincmb01cmp  11772  iccf1o  11773  fzosplitprm1  12015  hashprb  12571  swrd0fv  12790  eflt  14164  prmdiv  14726  vfermltl  14745  coprimeprodsq  14752  pythagtrip  14777  cshwshashlem2  15060  odinf  17207  odcl2  17209  slesolex  19700  tgtop11  19991  restntr  20191  hauscmplem  20414  icchmeo  21962  pi1xfr  22079  sinq12gt0  23455  tanord1  23479  axsegconlem6  24945  ghomlinOLD  26085  ghomidOLD  26086  nv1  26298  lnolin  26388  br8d  28211  ballotlemfc0  29318  ballotlemfcc  29319  ballotlemrv2  29347  ballotlemrv2OLD  29385  ghomfo  30302  ghomgsg  30304  br8  30389  br6  30390  br4  30391  ismtyima  32128  ismtybndlem  32131  cvrcmp2  32844  atcvrj2  32992  1cvratex  33032  lplnric  33111  lplnri1  33112  lnatexN  33338  ltrnateq  33741  ltrnatneq  33742  cdleme46f2g2  34054  cdleme46f2g1  34055  dibelval1st  34711  dibelval2nd  34714  dicelval1sta  34749  hlhilphllem  35524  jm2.17b  35805  hashgcdlem  36068  bi123impia  36839  sineq0ALT  37328  eliccre  37597  ioomidp  37609  iccpartiltu  38730  evengpop3  38887  pfxpfx  38950  repswpfx  38971  rnghmresel  39953  rhmresel  39999
  Copyright terms: Public domain W3C validator