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  2991  2reu5  3134  ordnbtwn  4663  onsucuni2  4805  poltletr  5260  tz6.12-1  5738  nfunsn  5752  smo11  6617  omlimcl  6812  th3qlem1  7001  omxpenlem  7200  fodomr  7249  fodomfib  7377  r1val1  7701  alephval3  7980  dfac5lem4  7996  dfac5  7998  axdc4lem  8324  fodomb  8393  distrlem1pr  8891  map2psrpr  8974  supsrlem  8975  eqle  9165  sumz  12504  divalglem8  12908  pospo  14418  lsmcv  16201  opsrtoslem1  16532  psrbagsuppfi  16553  hauscmplem  17457  ptbasfi  17601  hmphindis  17817  fbncp  17859  fgcl  17898  fixufil  17942  uffixfr  17943  mbfima  19512  mbfimaicc  19513  ig1pdvds  20087  uhgraun  21334  eupai  21677  spansncvi  23142  eigposi  23327  pjnormssi  23659  sumdmdlem  23909  rhmdvdsr  24244  rtrclind  25137  prod1  25259  dffix2  25700  ax5seglem4  25819  axcontlem2  25852  axcontlem4  25854  cgrdegen  25886  btwnconn1lem11  25979  btwnconn1lem12  25980  btwnconn1lem14  25982  isbnd2  26429  pm13.13a  27522  iotavalb  27545  2shwrdcom  28153  usgfiregdegfi  28235  usgreghash2spot  28316  biimpa21  28511  suctrALTcf  28888  suctrALTcfVD  28889  suctrALT3  28890  unisnALT  28892  bnj168  28951  bnj521  28958  bnj964  29168  bnj966  29169  bnj1398  29257  atcvrj0  30064  paddasslem5  30460
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