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

Theorem simplbi2com 655
 Description: A deduction eliminating a conjunct, similar to simplbi2 653. (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 653 . 2 (𝜓 → (𝜒𝜑))
32com12 32 1 (𝜒 → (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385 This theorem is referenced by:  elres  5355  xpidtr  5437  elovmpt2rab  6778  elovmpt2rab1  6779  inficl  8214  cfslb2n  8973  repswcshw  13409  cshw1  13419  bezoutlem1  15094  bezoutlem3  15096  modprmn0modprm0  15350  cnprest  20903  haust1  20966  lly1stc  21109  3cyclfrgrarn1  26539  dfon2lem9  30940  phpreu  32563  poimirlem26  32605  sb5ALT  37752  onfrALTlem2  37782  onfrALTlem2VD  38147  sb5ALTVD  38171  funcoressn  39856  ndmaovdistr  39936  reuccatpfxs1  40297  2elfz3nn0  40353  3cyclfrgrrn1  41455
 Copyright terms: Public domain W3C validator