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  3138  2reu5  3292  ordnbtwn  4954  poltletr  5388  tz6.12-1  5868  nfunsn  5883  onsucuni2  6650  smo11  7033  omlimcl  7225  omxpenlem  7616  fodomr  7666  fodomfib  7798  r1val1  8202  alephval3  8489  dfac5lem4  8505  dfac5  8507  axdc4lem  8833  fodomb  8902  distrlem1pr  9401  map2psrpr  9485  supsrlem  9486  eqle  9685  snopiswrd  12530  swrd0  12632  reuccats1lem  12679  repswswrd  12730  cshwidxmod  12748  sumz  13518  divalglem8  13930  pospo  15472  mgm2nsgrplem2  15906  lsmcv  17655  opsrtoslem1  18016  psrbagfsupp  18043  psrbagsuppfiOLD  18044  madugsum  19012  hauscmplem  19772  bwth  19776  ptbasfi  19948  hmphindis  20164  fbncp  20206  fgcl  20245  fixufil  20289  uffixfr  20290  mbfima  21905  mbfimaicc  21906  ig1pdvds  22443  tgldimor  23758  ax5seglem4  24100  axcontlem2  24133  axcontlem4  24135  uhgraun  24176  usgfiregdegfi  24776  eupai  24832  usgreghash2spot  24934  spansncvi  26435  eigposi  26620  pjnormssi  26952  sumdmdlem  27202  rhmdvdsr  27674  rtrclind  28938  prod1  29044  cgrdegen  29622  btwnconn1lem11  29715  btwnconn1lem12  29716  btwnconn1lem14  29718  fin2so  30008  dvasin  30071  isbnd2  30247  pm13.13a  31261  iotavalb  31284  fourierdlem40  31814  fourierdlem78  31852  2ffzoeq  32175  uhgun  32214  biimpa21  33050  suctrALTcf  33430  suctrALTcfVD  33431  suctrALT3  33432  unisnALT  33434  bnj168  33493  bnj521  33500  bnj964  33708  bnj966  33709  bnj1398  33797  bj-ccinftydisj  34318  atcvrj0  34854  paddasslem5  35250
  Copyright terms: Public domain W3C validator