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

Theorem biimpac 484
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 427 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  gencbvex2  3151  2reu5  3305  ordnbtwn  4957  poltletr  5387  tz6.12-1  5864  nfunsn  5879  onsucuni2  6642  smo11  7027  omlimcl  7219  omxpenlem  7611  fodomr  7661  fodomfib  7792  r1val1  8195  alephval3  8482  dfac5lem4  8498  dfac5  8500  axdc4lem  8826  fodomb  8895  distrlem1pr  9392  map2psrpr  9476  supsrlem  9477  eqle  9676  snopiswrd  12543  swrd0  12650  reuccats1lem  12696  repswswrd  12747  cshwidxmod  12765  rtrclind  12980  sumz  13626  prod1  13833  divalglem8  14142  pospo  15802  mgm2nsgrplem2  16236  lsmcv  17982  opsrtoslem1  18343  psrbagfsupp  18370  psrbagsuppfiOLD  18371  madugsum  19312  hauscmplem  20073  bwth  20077  ptbasfi  20248  hmphindis  20464  fbncp  20506  fgcl  20545  fixufil  20589  uffixfr  20590  mbfima  22205  mbfimaicc  22206  ig1pdvds  22743  tgldimor  24094  ax5seglem4  24437  axcontlem2  24470  axcontlem4  24472  uhgraun  24513  usgfiregdegfi  25113  eupai  25169  usgreghash2spot  25271  spansncvi  26768  eigposi  26953  pjnormssi  27285  sumdmdlem  27535  rhmdvdsr  28043  cgrdegen  29882  btwnconn1lem11  29975  btwnconn1lem12  29976  btwnconn1lem14  29978  fin2so  30280  dvasin  30343  isbnd2  30519  pm13.13a  31555  iotavalb  31578  fourierdlem40  32168  fourierdlem78  32206  2ffzoeq  32715  uhgun  32752  difmodm1lt  33389  nn0sumshdiglemA  33494  biimpa21  33736  suctrALTcf  34123  suctrALTcfVD  34124  suctrALT3  34125  unisnALT  34127  bnj168  34186  bnj521  34193  bnj964  34402  bnj966  34403  bnj1398  34491  bj-elid3  35002  bj-ccinftydisj  35016  atcvrj0  35549  paddasslem5  35945
  Copyright terms: Public domain W3C validator