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

Theorem simplbi2com 498
Description: A deduction eliminating a conjunct, similar to simplbi2 496. (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 496 . 2 (𝜓 → (𝜒𝜑))
32com12 32 1 (𝜒 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386
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 199  df-an 387
This theorem is referenced by:  elresOLD  5672  xpidtr  5760  elovmpt2rab  7140  elovmpt2rab1  7141  inficl  8600  cfslb2n  9405  repswcshw  13933  cshw1  13943  bezoutlem1  15629  bezoutlem3  15631  modprmn0modprm0  15883  cnprest  21464  haust1  21527  lly1stc  21670  3cyclfrgrrn1  27666  dfon2lem9  32234  phpreu  33936  poimirlem26  33979  sb5ALT  39569  onfrALTlem2  39590  onfrALTlem2VD  39943  sb5ALTVD  39967  funcoressn  41973  ndmaovdistr  42109  2elfz3nn0  42214
  Copyright terms: Public domain W3C validator