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

Theorem biimpac 473
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 216 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 419 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  gencbvex2  2943  2reu5  3086  ordnbtwn  4613  onsucuni2  4755  poltletr  5210  tz6.12-1  5688  nfunsn  5702  smo11  6563  omlimcl  6758  th3qlem1  6947  omxpenlem  7146  fodomr  7195  fodomfib  7323  r1val1  7646  alephval3  7925  dfac5lem4  7941  dfac5  7943  axdc4lem  8269  fodomb  8338  distrlem1pr  8836  map2psrpr  8919  supsrlem  8920  eqle  9110  sumz  12444  divalglem8  12848  pospo  14358  lsmcv  16141  opsrtoslem1  16472  psrbagsuppfi  16493  hauscmplem  17392  ptbasfi  17535  hmphindis  17751  fbncp  17793  fgcl  17832  fixufil  17876  uffixfr  17877  mbfima  19392  mbfimaicc  19393  ig1pdvds  19967  uhgraun  21214  eupai  21538  spansncvi  23003  eigposi  23188  pjnormssi  23520  sumdmdlem  23770  rhmdvdsr  24073  rtrclind  24929  prod1  25050  dffix2  25470  ax5seglem4  25586  axcontlem2  25619  axcontlem4  25621  cgrdegen  25653  btwnconn1lem11  25746  btwnconn1lem12  25747  btwnconn1lem14  25749  isbnd2  26184  pm13.13a  27277  iotavalb  27300  biimpa21  28000  suctrALTcf  28376  suctrALTcfVD  28377  suctrALT3  28378  unisnALT  28380  bnj168  28436  bnj521  28443  bnj964  28653  bnj966  28654  bnj1398  28742  atcvrj0  29543  paddasslem5  29939
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
  Copyright terms: Public domain W3C validator