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

Theorem simplbi2 502
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 227 . 2 ((𝜓𝜒) → 𝜑)
32ex 414 1 (𝜓 → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  simplbi2com  504  sspss  4064  neldif  4094  reuss2  4280  pssdifn0  4330  dfiun2g  4995  elinxp  5980  ordunidif  6371  eceqoveq  8768  infxpenlem  9956  ackbij1lem18  10180  isf32lem2  10297  ingru  10758  indpi  10850  nqereu  10872  elpq  12907  elfz0ubfz0  13552  elfzmlbp  13559  elfzo0z  13621  fzofzim  13626  fzo1fzo0n0  13630  elfzodifsumelfzo  13645  swrdswrd  14600  swrdccatin1  14620  swrd2lsw  14848  p1modz1  16150  dfgcd2  16434  algcvga  16462  pcprendvds  16719  restntr  22549  filconn  23250  filssufilg  23278  ufileu  23286  ufilen  23297  alexsubALTlem3  23416  blcld  23877  causs  24678  itg2addlem  25139  rplogsum  26891  sltres  27026  wlkonl1iedg  28655  trlf1  28688  spthdifv  28723  upgrwlkdvde  28727  usgr2pth  28754  pthdlem2  28758  uspgrn2crct  28795  crctcshwlkn0  28808  clwlkclwwlklem2  28986  clwwlknon0  29079  3spthd  29162  ofpreima2  31624  esumpinfval  32712  eulerpartlemf  33010  fin2so  36094  fdc  36233  lshpcmp  37479  lfl1  37561  frege124d  42107  onfrALTlem2  42902  3ornot23VD  43203  ordelordALTVD  43223  onfrALTlem2VD  43245  ndmaovass  45512  elfz2z  45621  lighneallem4  45876
  Copyright terms: Public domain W3C validator