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

Theorem simplbi2 656
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 218 . 2 ((𝜓𝜒) → 𝜑)
32ex 449 1 (𝜓 → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  simplbi2com  658  sspss  3848  neldif  3878  reuss2  4050  pssdifn0  4087  ordunidif  5934  eceqoveq  8019  infxpenlem  9026  ackbij1lem18  9251  isf32lem2  9368  ingru  9829  indpi  9921  nqereu  9943  elfz0ubfz0  12637  elfzmlbp  12644  elfzo0z  12704  fzofzim  12709  fzo1fzo0n0  12713  elfzodifsumelfzo  12728  ccat1st1st  13602  2swrd1eqwrdeq  13654  swrdswrd  13660  swrdccatin1  13683  swrd2lsw  13896  p1modz1  15189  dfgcd2  15465  algcvga  15494  pcprendvds  15747  restntr  21188  filconn  21888  filssufilg  21916  ufileu  21924  ufilen  21935  alexsubALTlem3  22054  blcld  22511  causs  23296  itg2addlem  23724  rplogsum  25415  wlkonl1iedg  26771  trlf1  26805  spthdifv  26839  upgrwlkdvde  26843  usgr2pth  26870  pthdlem2  26874  uspgrn2crct  26911  crctcshwlkn0  26924  clwlkclwwlklem2  27123  clwwlknon0  27240  3spthd  27328  ofpreima2  29775  esumpinfval  30444  eulerpartlemf  30741  sltres  32121  bj-elid2  33397  fin2so  33709  fdc  33854  lshpcmp  34778  lfl1  34860  frege124d  38555  onfrALTlem2  39263  3ornot23VD  39581  ordelordALTVD  39602  onfrALTlem2VD  39624  ndmaovass  41792  elfz2z  41835  lighneallem4  42037
  Copyright terms: Public domain W3C validator