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

Theorem biimp3a 1364
Description: Infer implication from a logical equivalence. Similar to biimpa 486. (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 486 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
323impa 1200 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  nn0addge1  10905  nn0addge2  10906  nn0sub2  10986  eluzp1p1  11173  uznn0sub  11179  uzinfi  11227  iocssre  11703  icossre  11704  iccssre  11705  lincmb01cmp  11762  iccf1o  11763  fzosplitprm1  12004  hashprb  12560  swrd0fv  12769  eflt  14138  prmdiv  14693  vfermltl  14712  coprimeprodsq  14719  pythagtrip  14744  cshwshashlem2  15027  odinf  17155  odcl2  17157  slesolex  19644  tgtop11  19935  restntr  20135  hauscmplem  20358  icchmeo  21891  pi1xfr  22005  sinq12gt0  23366  tanord1  23390  axsegconlem6  24839  ghomlinOLD  25978  ghomidOLD  25979  nv1  26191  lnolin  26281  br8d  28098  ballotlemfc0  29192  ballotlemfcc  29193  ballotlemrv2  29221  ghomfo  30138  ghomgsg  30140  br8  30224  br6  30225  br4  30226  ismtyima  31883  ismtybndlem  31886  cvrcmp2  32603  atcvrj2  32751  1cvratex  32791  lplnric  32870  lplnri1  32871  lnatexN  33097  ltrnateq  33500  ltrnatneq  33501  cdleme46f2g2  33813  cdleme46f2g1  33814  dibelval1st  34470  dibelval2nd  34473  dicelval1sta  34508  hlhilphllem  35283  jm2.17b  35565  hashgcdlem  35821  bi123impia  36530  sineq0ALT  37022  eliccre  37236  ioomidp  37248  iccpartiltu  38183  evengpop3  38340  pfxpfx  38403  repswpfx  38424  rnghmresel  38781  rhmresel  38827
  Copyright terms: Public domain W3C validator