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

Theorem simplbi2com 501
Description: A deduction eliminating a conjunct, similar to simplbi2 499. (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 499 . 2 (𝜓 → (𝜒𝜑))
32com12 32 1 (𝜒 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394
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 395
This theorem is referenced by:  xpidtr  6129  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  inficl  9450  cfslb2n  10293  repswcshw  14798  cshw1  14808  bezoutlem1  16518  bezoutlem3  16520  modprmn0modprm0  16779  insubm  18778  cnprest  23237  haust1  23300  lly1stc  23444  3cyclfrgrrn1  30167  dfon2lem9  35518  phpreu  37208  poimirlem26  37250  sb5ALT  44106  onfrALTlem2  44127  onfrALTlem2VD  44470  sb5ALTVD  44494  funcoressn  46562  ndmaovdistr  46725  2elfz3nn0  46834
  Copyright terms: Public domain W3C validator