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

Theorem simplbiim 659
Description: Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 26-Mar-2022.)
Hypotheses
Ref Expression
simplbiim.1 (𝜑 ↔ (𝜓𝜒))
simplbiim.2 (𝜒𝜃)
Assertion
Ref Expression
simplbiim (𝜑𝜃)

Proof of Theorem simplbiim
StepHypRef Expression
1 simplbiim.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21simprbi 479 . 2 (𝜑𝜒)
3 simplbiim.2 . 2 (𝜒𝜃)
42, 3syl 17 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:  invdisjrab  4671  solin  5087  xpidtr  5553  elpredim  5730  mpt2difsnif  6795  ixpn0  7982  zltaddlt1le  12362  oddnn02np1  15119  sumeven  15157  dvdsprmpweqnn  15636  sgrpass  17337  zringndrg  19886  pmatcoe1fsupp  20554  t1sncld  21178  regsep  21186  nrmsep3  21207  ncvsprp  22998  ncvsm1  23000  ncvsdif  23001  ncvspi  23002  ncvspds  23007  lgsqrlem4  25119  vtxdginducedm1lem4  26494  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  0spth  27104  eucrctshift  27221  frcond1  27246  2pthfrgr  27264  frgrncvvdeqlem7  27285  frgrncvvdeq  27289  frgrwopreglem3  27294  frgrwopreglem5lem  27300  frgr2wwlk1  27309  numclwlk1lem2f1  27347  stcltr1i  29261  bnj570  31101  bnj1145  31187  bnj1398  31228  bnj1442  31243  sconnpht  31337  poimirlem25  33564  2reu1  41507  lighneallem2  41848  fdmdifeqresdif  42445
  Copyright terms: Public domain W3C validator