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

Theorem simplbi2com 505
 Description: A deduction eliminating a conjunct, similar to simplbi2 503. (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 503 . 2 (𝜓 → (𝜒𝜑))
32com12 32 1 (𝜒 → (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  xpidtr  5981  elovmporab  7390  elovmporab1w  7391  elovmporab1  7392  inficl  8888  cfslb2n  9689  repswcshw  14173  cshw1  14183  bezoutlem1  15886  bezoutlem3  15888  modprmn0modprm0  16143  insubm  17982  cnprest  21896  haust1  21959  lly1stc  22103  3cyclfrgrrn1  28063  dfon2lem9  33036  phpreu  34875  poimirlem26  34917  sb5ALT  40857  onfrALTlem2  40878  onfrALTlem2VD  41221  sb5ALTVD  41245  funcoressn  43276  ndmaovdistr  43405  2elfz3nn0  43515
 Copyright terms: Public domain W3C validator