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

Theorem simplbi2com 656
 Description: A deduction eliminating a conjunct, similar to simplbi2 654. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.)
Hypothesis
Ref Expression
simplbi2com.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
simplbi2com (𝜒 → (𝜓𝜑))

Proof of Theorem simplbi2com
StepHypRef Expression
1 simplbi2com.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21simplbi2 654 . 2 (𝜓 → (𝜒𝜑))
32com12 32 1 (𝜒 → (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384 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 386 This theorem is referenced by:  elres  5399  xpidtr  5482  elovmpt2rab  6840  elovmpt2rab1  6841  inficl  8283  cfslb2n  9042  repswcshw  13503  cshw1  13513  bezoutlem1  15191  bezoutlem3  15193  modprmn0modprm0  15447  cnprest  21016  haust1  21079  lly1stc  21222  3cyclfrgrrn1  27030  dfon2lem9  31432  phpreu  33060  poimirlem26  33102  sb5ALT  38248  onfrALTlem2  38278  onfrALTlem2VD  38643  sb5ALTVD  38667  funcoressn  40537  ndmaovdistr  40617  2elfz3nn0  40649  reuccatpfxs1  40759
 Copyright terms: Public domain W3C validator