MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplbi2 Structured version   Visualization version   GIF version

Theorem simplbi2 501
Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)
Hypothesis
Ref Expression
simplbi2.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
simplbi2 (𝜓 → (𝜒𝜑))

Proof of Theorem simplbi2
StepHypRef Expression
1 simplbi2.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21biimpri 229 . 2 ((𝜓𝜒) → 𝜑)
32ex 413 1 (𝜓 → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  simplbi2com  503  sspss  3997  neldif  4027  reuss2  4203  pssdifn0  4245  elinxp  5771  ordunidif  6114  eceqoveq  8252  infxpenlem  9285  ackbij1lem18  9505  isf32lem2  9622  ingru  10083  indpi  10175  nqereu  10197  elpq  12224  elfz0ubfz0  12861  elfzmlbp  12868  elfzo0z  12929  fzofzim  12934  fzo1fzo0n0  12938  elfzodifsumelfzo  12953  ccat1st1st  13826  swrdswrd  13903  swrdccatin1  13923  swrd2lsw  14150  p1modz1  15447  dfgcd2  15723  algcvga  15752  pcprendvds  16006  restntr  21474  filconn  22175  filssufilg  22203  ufileu  22211  ufilen  22222  alexsubALTlem3  22341  blcld  22798  causs  23584  itg2addlem  24042  rplogsum  25785  wlkonl1iedg  27129  trlf1  27165  spthdifv  27201  upgrwlkdvde  27205  usgr2pth  27232  pthdlem2  27236  uspgrn2crct  27273  crctcshwlkn0  27286  clwlkclwwlklem2  27465  clwwlknon0  27559  3spthd  27642  ofpreima2  30101  esumpinfval  30949  eulerpartlemf  31245  sltres  32779  bj-epelg  33978  bj-elid2  34047  fin2so  34429  fdc  34571  lshpcmp  35674  lfl1  35756  frege124d  39610  onfrALTlem2  40438  3ornot23VD  40739  ordelordALTVD  40759  onfrALTlem2VD  40781  ndmaovass  42941  elfz2z  43051  lighneallem4  43277
  Copyright terms: Public domain W3C validator