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  10198  nn0addge2  10199  nn0sub2  10267  eluzp1p1  10443  uznn0sub  10449  iocssre  10922  icossre  10923  iccssre  10924  lincmb01cmp  10970  iccf1o  10971  hashprb  11595  eflt  12645  prmdiv  13101  coprimeprodsq  13110  pythagtrip  13135  spwcl  14589  odinf  15126  odcl2  15128  tgtop11  16970  restntr  17168  hauscmplem  17391  icchmeo  18837  pi1xfr  18951  sinq12gt0  20282  tanord1  20306  ghomlin  21800  ghomid  21801  nv1  22013  lnolin  22103  ballotlemfc0  24529  ballotlemfcc  24530  ballotlemrv2  24558  ghomfo  24881  ghomgsg  24883  br8  25137  br6  25138  br4  25139  axsegconlem6  25575  ismtyima  26203  ismtybndlem  26206  jm2.17b  26717  hashgcdlem  27185  bi123impia  27918  cvrcmp2  29399  atcvrj2  29547  1cvratex  29587  lplnric  29666  lplnri1  29667  lnatexN  29893  ltrnateq  30295  ltrnatneq  30296  cdleme46f2g2  30607  cdleme46f2g1  30608  dibelval1st  31264  dibelval2nd  31267  dicelval1sta  31302  hlhilphllem  32077
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