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

Theorem simplbiim 658
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 482 . 2 ((𝜓𝜒) → 𝜃)
41, 3sylbi 207 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  invdisjrab  4607  solin  5023  xpidtr  5482  elpredim  5656  mpt2difsnif  6713  ixpn0  7892  zltaddlt1le  12274  oddnn02np1  15007  sumeven  15045  dvdsprmpweqnn  15524  sgrpass  17222  zringndrg  19770  pmatcoe1fsupp  20438  t1sncld  21053  regsep  21061  nrmsep3  21082  ncvsprp  22875  ncvsm1  22877  ncvsdif  22878  ncvspi  22879  ncvspds  22884  lgsqrlem4  24991  isclwwlksnx  26773  hashecclwwlksn1  26837  umgrhashecclwwlk  26838  0spth  26870  eucrctshift  26986  frcond1  27013  2pthfrgr  27029  frgrncvvdeqlem3  27046  frgrncvvdeqlemA  27051  frgrncvvdeq  27055  frgr2wwlk1  27069  frgr2wwlkeqm  27071  stcltr1i  29003  bnj570  30718  bnj1145  30804  bnj1398  30845  bnj1442  30860  sconnpht  30954  poimirlem25  33101  2reu1  40516  lighneallem2  40848
  Copyright terms: Public domain W3C validator