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

Theorem biimpac 486
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimpac  |-  ( ( ps  /\  ph )  ->  ch )

Proof of Theorem biimpac
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpcd 224 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 429 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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
This theorem is referenced by:  gencbvex2  3158  2reu5  3312  ordnbtwn  4968  poltletr  5402  tz6.12-1  5882  nfunsn  5897  onsucuni2  6653  smo11  7035  omlimcl  7227  omxpenlem  7618  fodomr  7668  fodomfib  7800  r1val1  8204  alephval3  8491  dfac5lem4  8507  dfac5  8509  axdc4lem  8835  fodomb  8904  distrlem1pr  9403  map2psrpr  9487  supsrlem  9488  eqle  9687  snopiswrd  12522  swrd0  12621  reuccats1lem  12668  repswswrd  12719  cshwidxmod  12737  sumz  13507  divalglem8  13917  pospo  15460  lsmcv  17587  opsrtoslem1  17947  psrbagfsupp  17974  psrbagsuppfiOLD  17975  madugsum  18940  hauscmplem  19700  bwth  19704  ptbasfi  19845  hmphindis  20061  fbncp  20103  fgcl  20142  fixufil  20186  uffixfr  20187  mbfima  21802  mbfimaicc  21803  ig1pdvds  22340  tgldimor  23649  ax5seglem4  23939  axcontlem2  23972  axcontlem4  23974  uhgraun  24015  usgfiregdegfi  24615  eupai  24671  usgreghash2spot  24774  spansncvi  26274  eigposi  26459  pjnormssi  26791  sumdmdlem  27041  rhmdvdsr  27499  rtrclind  28575  prod1  28681  cgrdegen  29259  btwnconn1lem11  29352  btwnconn1lem12  29353  btwnconn1lem14  29355  fin2so  29645  dvasin  29708  isbnd2  29910  pm13.13a  30920  iotavalb  30943  lptioo2  31201  lptioo1  31202  uhgun  31875  biimpa21  32440  suctrALTcf  32820  suctrALTcfVD  32821  suctrALT3  32822  unisnALT  32824  bnj168  32883  bnj521  32890  bnj964  33098  bnj966  33099  bnj1398  33187  bj-ccinftydisj  33706  atcvrj0  34242  paddasslem5  34638
  Copyright terms: Public domain W3C validator