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

Theorem biimpac 483
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  3006  2reu5  3156  ordnbtwn  4796  poltletr  5221  tz6.12-1  5694  nfunsn  5709  onsucuni2  6434  smo11  6811  omlimcl  7005  th3qlem1  7194  omxpenlem  7400  fodomr  7450  fodomfib  7579  r1val1  7981  alephval3  8268  dfac5lem4  8284  dfac5  8286  axdc4lem  8612  fodomb  8681  distrlem1pr  9181  map2psrpr  9264  supsrlem  9265  eqle  9464  snopiswrd  12226  wrdlenfi  12241  swrd0  12310  repswswrd  12405  cshwidxmod  12423  sumz  13182  divalglem8  13586  pospo  15125  lsmcv  17143  opsrtoslem1  17496  psrbagfsupp  17519  psrbagsuppfiOLD  17520  madugsum  18290  hauscmplem  18850  bwth  18854  ptbasfi  18995  hmphindis  19211  fbncp  19253  fgcl  19292  fixufil  19336  uffixfr  19337  mbfima  20951  mbfimaicc  20952  ig1pdvds  21532  tgldimor  22836  ax5seglem4  23000  axcontlem2  23033  axcontlem4  23035  uhgraun  23067  eupai  23410  spansncvi  24877  eigposi  25062  pjnormssi  25394  sumdmdlem  25644  rhmdvdsr  26138  rtrclind  27197  prod1  27303  cgrdegen  27881  btwnconn1lem11  27974  btwnconn1lem12  27975  btwnconn1lem14  27977  fin2so  28257  dvasin  28321  isbnd2  28523  pm13.13a  29503  iotavalb  29526  usgfiregdegfi  30371  usgreghash2spot  30505  biimpa21  30976  suctrALTcf  31357  suctrALTcfVD  31358  suctrALT3  31359  unisnALT  31361  bnj168  31420  bnj521  31427  bnj964  31635  bnj966  31636  bnj1398  31724  bj-ccinftydisj  32113  atcvrj0  32642  paddasslem5  33038
  Copyright terms: Public domain W3C validator