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

Theorem biimpac 486
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  3038  2reu5  3188  ordnbtwn  4830  poltletr  5254  tz6.12-1  5727  nfunsn  5742  onsucuni2  6466  smo11  6846  omlimcl  7038  th3qlem1  7227  omxpenlem  7433  fodomr  7483  fodomfib  7612  r1val1  8014  alephval3  8301  dfac5lem4  8317  dfac5  8319  axdc4lem  8645  fodomb  8714  distrlem1pr  9215  map2psrpr  9298  supsrlem  9299  eqle  9498  snopiswrd  12264  wrdlenfi  12279  swrd0  12348  repswswrd  12443  cshwidxmod  12461  sumz  13220  divalglem8  13625  pospo  15164  lsmcv  17244  opsrtoslem1  17587  psrbagfsupp  17614  psrbagsuppfiOLD  17615  madugsum  18471  hauscmplem  19031  bwth  19035  ptbasfi  19176  hmphindis  19392  fbncp  19434  fgcl  19473  fixufil  19517  uffixfr  19518  mbfima  21132  mbfimaicc  21133  ig1pdvds  21670  tgldimor  22977  ax5seglem4  23200  axcontlem2  23233  axcontlem4  23235  uhgraun  23267  eupai  23610  spansncvi  25077  eigposi  25262  pjnormssi  25594  sumdmdlem  25844  rhmdvdsr  26308  rtrclind  27373  prod1  27479  cgrdegen  28057  btwnconn1lem11  28150  btwnconn1lem12  28151  btwnconn1lem14  28153  fin2so  28442  dvasin  28506  isbnd2  28708  pm13.13a  29687  iotavalb  29710  usgfiregdegfi  30554  usgreghash2spot  30688  biimpa21  31374  suctrALTcf  31754  suctrALTcfVD  31755  suctrALT3  31756  unisnALT  31758  bnj168  31817  bnj521  31824  bnj964  32032  bnj966  32033  bnj1398  32121  bj-ccinftydisj  32632  atcvrj0  33168  paddasslem5  33564
  Copyright terms: Public domain W3C validator