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

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

Proof of Theorem simplbiim
StepHypRef Expression
1 simplbiim.1 . 2 (𝜑 ↔ (𝜓𝜒))
2 simplbiim.2 . . 3 (𝜒𝜃)
32adantl 481 . 2 ((𝜓𝜒) → 𝜃)
41, 3sylbi 206 1 (𝜑𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385 This theorem is referenced by:  invdisjrab  4572  solin  4982  xpidtr  5437  elpredim  5609  zltaddlt1le  12195  oddnn02np1  14910  sumeven  14948  dvdsprmpweqnn  15427  zringndrg  19657  pmatcoe1fsupp  20325  ncvsprp  22760  ncvsm1  22762  ncvsdif  22763  ncvspi  22764  ncvspds  22769  lgsqrlem4  24874  bnj570  30229  bnj1145  30315  bnj1398  30356  bnj1442  30371  poimirlem25  32604  lighneallem2  40061  isclwwlksnx  41197  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  eucrctshift  41411  2pthfrgr  41454  frgrncvvdeqlem3  41471  frgrncvvdeqlemA  41476  frgrncvvdeq  41480  frgr2wwlk1  41494  frgr2wwlkeqm  41496
 Copyright terms: Public domain W3C validator