![]() |
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 227 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑) |
3 | 2 | ex 412 | 1 ⊢ (𝜓 → (𝜒 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ 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 206 df-an 396 |
This theorem is referenced by: simplbi2com 502 sspss 4099 neldif 4129 reuss2 4315 pssdifn0 4365 dfiun2g 5033 elinxp 6019 ordunidif 6413 eceqoveq 8822 infxpenlem 10014 ackbij1lem18 10238 isf32lem2 10355 ingru 10816 indpi 10908 nqereu 10930 elpq 12966 elfz0ubfz0 13612 elfzmlbp 13619 elfzo0z 13681 fzofzim 13686 fzo1fzo0n0 13690 elfzodifsumelfzo 13705 swrdswrd 14662 swrdccatin1 14682 swrd2lsw 14910 p1modz1 16211 dfgcd2 16495 algcvga 16523 pcprendvds 16780 restntr 22919 filconn 23620 filssufilg 23648 ufileu 23656 ufilen 23667 alexsubALTlem3 23786 blcld 24247 causs 25059 itg2addlem 25521 rplogsum 27281 sltres 27416 wlkonl1iedg 29204 trlf1 29237 spthdifv 29272 upgrwlkdvde 29276 usgr2pth 29303 pthdlem2 29307 uspgrn2crct 29344 crctcshwlkn0 29357 clwlkclwwlklem2 29535 clwwlknon0 29628 3spthd 29711 ofpreima2 32173 esumpinfval 33384 eulerpartlemf 33682 fin2so 36791 fdc 36929 lshpcmp 38174 lfl1 38256 frege124d 42827 onfrALTlem2 43622 3ornot23VD 43923 ordelordALTVD 43943 onfrALTlem2VD 43965 ndmaovass 46225 elfz2z 46334 lighneallem4 46589 |
Copyright terms: Public domain | W3C validator |