| 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 228 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑) |
| 3 | 2 | ex 412 | 1 ⊢ (𝜓 → (𝜒 → 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: simplbi2com 502 sspss 4102 neldif 4134 reuss2 4326 pssdifn0 4368 dfiun2g 5030 elinxp 6037 ordunidif 6433 eceqoveq 8862 infxpenlem 10053 ackbij1lem18 10276 isf32lem2 10394 ingru 10855 indpi 10947 nqereu 10969 elpq 13017 elfz0ubfz0 13672 elfzmlbp 13679 elfzo0z 13741 fzofzim 13749 fzo1fzo0n0 13754 elfzodifsumelfzo 13770 swrdswrd 14743 swrdccatin1 14763 swrd2lsw 14991 p1modz1 16297 dfgcd2 16583 algcvga 16616 pcprendvds 16878 restntr 23190 filconn 23891 filssufilg 23919 ufileu 23927 ufilen 23938 alexsubALTlem3 24057 blcld 24518 causs 25332 itg2addlem 25793 rplogsum 27571 sltres 27707 wlkonl1iedg 29683 trlf1 29716 spthdifv 29753 upgrwlkdvde 29757 usgr2pth 29784 pthdlem2 29788 uspgrn2crct 29828 crctcshwlkn0 29841 clwlkclwwlklem2 30019 clwwlknon0 30112 3spthd 30195 ofpreima2 32676 esumpinfval 34074 eulerpartlemf 34372 fin2so 37614 fdc 37752 lshpcmp 38989 lfl1 39071 frege124d 43774 onfrALTlem2 44566 3ornot23VD 44867 ordelordALTVD 44887 onfrALTlem2VD 44909 ndmaovass 47218 elfz2z 47327 lighneallem4 47597 |
| Copyright terms: Public domain | W3C validator |