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

Theorem biimpac 472
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 215 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 418 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  gencbvex2  2844  2reu5  2986  trsuc2OLD  4493  ordnbtwn  4499  onsucuni2  4641  poltletr  5094  nfunsn  5574  smo11  6397  omlimcl  6592  th3qlem1  6780  omxpenlem  6979  fodomr  7028  fodomfib  7152  r1val1  7474  alephval3  7753  dfac5lem4  7769  dfac5  7771  axdc4lem  8097  fodomb  8167  distrlem1pr  8665  map2psrpr  8748  supsrlem  8749  eqle  8939  sumz  12211  divalglem8  12615  pospo  14123  lsmcv  15910  opsrtoslem1  16241  psrbagsuppfi  16262  hauscmplem  17149  ptbasfi  17292  hmphindis  17504  fbncp  17550  fgcl  17589  fixufil  17633  uffixfr  17634  mbfima  19003  mbfimaicc  19004  ig1pdvds  19578  spansncvi  22247  eigposi  22432  pjnormssi  22764  sumdmdlem  23014  eupai  23898  rtrclind  24061  prod1  24169  dffix2  24516  ax5seglem4  24632  axcontlem2  24665  axcontlem4  24667  cgrdegen  24699  btwnconn1lem11  24792  btwnconn1lem12  24793  btwnconn1lem14  24795  limptlimpr2lem2  25678  clscnc  26113  isbnd2  26610  pm13.13a  27710  iotavalb  27733  suctrALTcf  29014  suctrALTcfVD  29015  suctrALT3  29016  unisnALT  29018  suctrALT4  29020  bnj168  29074  bnj521  29081  bnj964  29291  bnj966  29292  bnj1398  29380  a12study4  29739  atcvrj0  30239  paddasslem5  30635
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 177  df-an 360
  Copyright terms: Public domain W3C validator