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

Theorem simplbi2com 658
Description: A deduction eliminating a conjunct, similar to simplbi2 656. (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 656 . 2 (𝜓 → (𝜒𝜑))
32com12 32 1 (𝜒 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 385
This theorem is referenced by:  elres  5581  xpidtr  5664  elovmpt2rab  7033  elovmpt2rab1  7034  inficl  8484  cfslb2n  9253  repswcshw  13729  cshw1  13739  bezoutlem1  15429  bezoutlem3  15431  modprmn0modprm0  15685  cnprest  21266  haust1  21329  lly1stc  21472  3cyclfrgrrn1  27410  dfon2lem9  31972  phpreu  33675  poimirlem26  33717  sb5ALT  39202  onfrALTlem2  39232  onfrALTlem2VD  39593  sb5ALTVD  39617  funcoressn  41682  ndmaovdistr  41762  2elfz3nn0  41805  reuccatpfxs1  41913
  Copyright terms: Public domain W3C validator