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

Theorem biimpac 493
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 232 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 435 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  gencbvex2  3060  2reu5  3215  poltletr  5209  ordnbtwn  5491  tz6.12-1  5863  nfunsn  5878  onsucuni2  6648  smo11  7069  omlimcl  7265  omxpenlem  7659  fodomr  7709  fodomfib  7837  r1val1  8243  alephval3  8527  dfac5lem4  8543  dfac5  8545  axdc4lem  8871  fodomb  8940  distrlem1pr  9436  map2psrpr  9520  supsrlem  9521  eqle  9722  snopiswrd  12675  swrd0  12788  reuccats1lem  12834  repswswrd  12885  cshwidxmod  12903  rtrclind  13138  sumz  13798  prod1  14008  divalglem8  14390  pospo  16229  mgm2nsgrplem2  16663  lsmcv  18374  opsrtoslem1  18717  psrbagfsupp  18742  madugsum  19678  hauscmplem  20431  bwth  20435  ptbasfi  20606  hmphindis  20822  fbncp  20864  fgcl  20903  fixufil  20947  uffixfr  20948  mbfima  22599  mbfimaicc  22600  ig1pdvds  23139  ig1pdvdsOLD  23145  tgldimor  24557  ax5seglem4  24973  axcontlem2  25006  axcontlem4  25008  uhgraun  25049  usgfiregdegfi  25650  eupai  25706  usgreghash2spot  25808  spansncvi  27316  eigposi  27500  pjnormssi  27832  sumdmdlem  28082  rhmdvdsr  28587  bnj168  29543  bnj521  29550  bnj964  29759  bnj966  29760  bnj1398  29848  cgrdegen  30776  btwnconn1lem11  30869  btwnconn1lem12  30870  btwnconn1lem14  30872  bj-elid3  31643  bj-ccinftydisj  31656  phpreu  31930  fin2so  31933  poimirlem26  31967  poimirlem28  31969  dvasin  32029  isbnd2  32116  atcvrj0  32994  paddasslem5  33390  pm13.13a  36758  iotavalb  36781  biimpa21  36934  suctrALTcf  37315  suctrALTcfVD  37316  suctrALT3  37317  unisnALT  37319  xreqle  37570  fourierdlem40  38066  fourierdlem78  38104  fdisjdmun  38720  funopsn  39111  2ffzoeq  39157  cusgrfi  39620  fusgrregdegfi  39687  rusgr1vtxlem  39703  uhgun  40016  difmodm1lt  40649  nn0sumshdiglemA  40754
  Copyright terms: Public domain W3C validator