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  2831  2reu5  2973  trsuc2OLD  4477  ordnbtwn  4483  onsucuni2  4625  poltletr  5078  nfunsn  5558  smo11  6381  omlimcl  6576  th3qlem1  6764  omxpenlem  6963  fodomr  7012  fodomfib  7136  r1val1  7458  alephval3  7737  dfac5lem4  7753  dfac5  7755  axdc4lem  8081  fodomb  8151  distrlem1pr  8649  map2psrpr  8732  supsrlem  8733  eqle  8923  sumz  12195  divalglem8  12599  pospo  14107  lsmcv  15894  opsrtoslem1  16225  psrbagsuppfi  16246  hauscmplem  17133  ptbasfi  17276  hmphindis  17488  fbncp  17534  fgcl  17573  fixufil  17617  uffixfr  17618  mbfima  18987  mbfimaicc  18988  ig1pdvds  19562  spansncvi  22231  eigposi  22416  pjnormssi  22748  sumdmdlem  22998  eupai  23883  rtrclind  24046  dffix2  24445  ax5seglem4  24560  axcontlem2  24593  axcontlem4  24595  cgrdegen  24627  btwnconn1lem11  24720  btwnconn1lem12  24721  btwnconn1lem14  24723  limptlimpr2lem2  25575  clscnc  26010  isbnd2  26507  pm13.13a  27607  iotavalb  27630  suctrALTcf  28698  suctrALTcfVD  28699  suctrALT3  28700  unisnALT  28702  suctrALT4  28704  bnj168  28758  bnj521  28765  bnj964  28975  bnj966  28976  bnj1398  29064  a12study4  29117  atcvrj0  29617  paddasslem5  30013
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