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

Theorem simplbi2com 504
Description: A deduction eliminating a conjunct, similar to simplbi2 502. (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 502 . 2 (𝜓 → (𝜒𝜑))
32com12 32 1 (𝜒 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 398
This theorem is referenced by:  xpidtr  6080  elovmporab  7603  elovmporab1w  7604  elovmporab1  7605  inficl  9369  cfslb2n  10212  repswcshw  14709  cshw1  14719  bezoutlem1  16428  bezoutlem3  16430  modprmn0modprm0  16687  insubm  18637  cnprest  22663  haust1  22726  lly1stc  22870  3cyclfrgrrn1  29278  dfon2lem9  34429  phpreu  36112  poimirlem26  36154  sb5ALT  42899  onfrALTlem2  42920  onfrALTlem2VD  43263  sb5ALTVD  43287  funcoressn  45366  ndmaovdistr  45529  2elfz3nn0  45638
  Copyright terms: Public domain W3C validator