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

Theorem biimp3a 1313
Description: Infer implication from a logical equivalence. Similar to biimpa 481. (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 481 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
323impa 1177 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 960
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 962
This theorem is referenced by:  nn0addge1  10622  nn0addge2  10623  nn0sub2  10701  eluzp1p1  10882  uznn0sub  10888  iocssre  11371  icossre  11372  iccssre  11373  lincmb01cmp  11424  iccf1o  11425  hashprb  12153  swrd0fv  12331  eflt  13397  prmdiv  13856  coprimeprodsq  13872  pythagtrip  13897  cshwshashlem2  14119  odinf  16057  odcl2  16059  slesolex  18447  tgtop11  18546  restntr  18745  hauscmplem  18968  icchmeo  20472  pi1xfr  20586  sinq12gt0  21928  tanord1  21952  axsegconlem6  23103  ghomlin  23786  ghomid  23787  nv1  23999  lnolin  24089  br8d  25877  ballotlemfc0  26805  ballotlemfcc  26806  ballotlemrv2  26834  ghomfo  27239  ghomgsg  27241  br8  27495  br6  27496  br4  27497  ismtyima  28627  ismtybndlem  28630  jm2.17b  29229  hashgcdlem  29490  fzosplitprm1  30149  bi123impia  31026  sineq0ALT  31507  cvrcmp2  32651  atcvrj2  32799  1cvratex  32839  lplnric  32918  lplnri1  32919  lnatexN  33145  ltrnateq  33547  ltrnatneq  33548  cdleme46f2g2  33859  cdleme46f2g1  33860  dibelval1st  34516  dibelval2nd  34519  dicelval1sta  34554  hlhilphllem  35329
  Copyright terms: Public domain W3C validator