![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simplbiim | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
simplbiim.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
simplbiim.2 | ⊢ (𝜒 → 𝜃) |
Ref | Expression |
---|---|
simplbiim | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplbiim.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | 1 | simprbi 492 | . 2 ⊢ (𝜑 → 𝜒) |
3 | simplbiim.2 | . 2 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: invdisjrab 4860 solin 5286 xpidtr 5760 elpredim 5932 fvn0ssdmfun 6599 mpt2difsnif 7013 ixpn0 8207 zltaddlt1le 12617 oddnn02np1 15446 sumeven 15484 dvdsprmpweqnn 15960 sgrpass 17643 zringndrg 20198 pmatcoe1fsupp 20876 t1sncld 21501 regsep 21509 nrmsep3 21530 ncvsprp 23321 ncvsm1 23323 ncvsdif 23324 ncvspi 23325 ncvspds 23330 lgsqrlem4 25487 vtxdginducedm1lem4 26840 hashecclwwlkn1 27430 umgrhashecclwwlk 27431 0spth 27502 eucrctshift 27620 frcond1 27647 2pthfrgr 27665 frgrncvvdeqlem7 27686 frgrncvvdeq 27690 frgrwopreglem3 27695 frgrwopreglem5lem 27701 frgr2wwlk1 27710 numclwwlk1lem2f1 27748 numclwwlk1lem2f1OLD 27753 hhcms 28615 stcltr1i 29688 bnj570 31521 bnj1145 31607 bnj1398 31648 bnj1442 31663 sconnpht 31757 poimirlem25 33978 funressnfv 41974 funressnvmo 41976 funressnvmoOLD 41977 2reu1 42011 frnvafv2v 42138 dfatbrafv2b 42147 lighneallem2 42353 fdmdifeqresdif 42967 lindslinindsimp1 43093 |
Copyright terms: Public domain | W3C validator |