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

Theorem simplbi2com 497
Description: A deduction eliminating a conjunct, similar to simplbi2 495. (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 495 . 2 (𝜓 → (𝜒𝜑))
32com12 32 1 (𝜒 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385
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 386
This theorem is referenced by:  elresOLD  5646  xpidtr  5736  elovmpt2rab  7114  elovmpt2rab1  7115  inficl  8573  cfslb2n  9378  repswcshw  13897  cshw1  13907  bezoutlem1  15591  bezoutlem3  15593  modprmn0modprm0  15845  cnprest  21422  haust1  21485  lly1stc  21628  3cyclfrgrrn1  27634  dfon2lem9  32208  phpreu  33882  poimirlem26  33924  sb5ALT  39511  onfrALTlem2  39532  onfrALTlem2VD  39885  sb5ALTVD  39909  funcoressn  41925  ndmaovdistr  42061  2elfz3nn0  42166
  Copyright terms: Public domain W3C validator