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

Theorem biimp3a 1318
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 1182 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  nn0addge1  10647  nn0addge2  10648  nn0sub2  10726  eluzp1p1  10907  uznn0sub  10913  iocssre  11396  icossre  11397  iccssre  11398  lincmb01cmp  11449  iccf1o  11450  hashprb  12178  swrd0fv  12356  eflt  13422  prmdiv  13881  coprimeprodsq  13897  pythagtrip  13922  cshwshashlem2  14144  odinf  16085  odcl2  16087  slesolex  18510  tgtop11  18609  restntr  18808  hauscmplem  19031  icchmeo  20535  pi1xfr  20649  sinq12gt0  21991  tanord1  22015  axsegconlem6  23190  ghomlin  23873  ghomid  23874  nv1  24086  lnolin  24176  br8d  25964  ballotlemfc0  26897  ballotlemfcc  26898  ballotlemrv2  26926  ghomfo  27332  ghomgsg  27334  br8  27588  br6  27589  br4  27590  ismtyima  28728  ismtybndlem  28731  jm2.17b  29330  hashgcdlem  29591  fzosplitprm1  30250  bi123impia  31289  sineq0ALT  31769  cvrcmp2  33025  atcvrj2  33173  1cvratex  33213  lplnric  33292  lplnri1  33293  lnatexN  33519  ltrnateq  33921  ltrnatneq  33922  cdleme46f2g2  34233  cdleme46f2g1  34234  dibelval1st  34890  dibelval2nd  34893  dicelval1sta  34928  hlhilphllem  35703
  Copyright terms: Public domain W3C validator