![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simplbi2 | Structured version Visualization version GIF version |
Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.) |
Ref | Expression |
---|---|
simplbi2.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
simplbi2 | ⊢ (𝜓 → (𝜒 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplbi2.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | 1 | biimpri 218 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑) |
3 | 2 | ex 449 | 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: simplbi2com 658 sspss 3848 neldif 3878 reuss2 4050 pssdifn0 4087 ordunidif 5934 eceqoveq 8019 infxpenlem 9026 ackbij1lem18 9251 isf32lem2 9368 ingru 9829 indpi 9921 nqereu 9943 elfz0ubfz0 12637 elfzmlbp 12644 elfzo0z 12704 fzofzim 12709 fzo1fzo0n0 12713 elfzodifsumelfzo 12728 ccat1st1st 13602 2swrd1eqwrdeq 13654 swrdswrd 13660 swrdccatin1 13683 swrd2lsw 13896 p1modz1 15189 dfgcd2 15465 algcvga 15494 pcprendvds 15747 restntr 21188 filconn 21888 filssufilg 21916 ufileu 21924 ufilen 21935 alexsubALTlem3 22054 blcld 22511 causs 23296 itg2addlem 23724 rplogsum 25415 wlkonl1iedg 26771 trlf1 26805 spthdifv 26839 upgrwlkdvde 26843 usgr2pth 26870 pthdlem2 26874 uspgrn2crct 26911 crctcshwlkn0 26924 clwlkclwwlklem2 27123 clwwlknon0 27240 3spthd 27328 ofpreima2 29775 esumpinfval 30444 eulerpartlemf 30741 sltres 32121 bj-elid2 33397 fin2so 33709 fdc 33854 lshpcmp 34778 lfl1 34860 frege124d 38555 onfrALTlem2 39263 3ornot23VD 39581 ordelordALTVD 39602 onfrALTlem2VD 39624 ndmaovass 41792 elfz2z 41835 lighneallem4 42037 |
Copyright terms: Public domain | W3C validator |