![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpli | Structured version Visualization version GIF version |
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.) |
Ref | Expression |
---|---|
simpli.1 | ⊢ (𝜑 ∧ 𝜓) |
Ref | Expression |
---|---|
simpli | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpli.1 | . 2 ⊢ (𝜑 ∧ 𝜓) | |
2 | simpl 472 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∧ 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: exan 1828 exanOLD 1829 pwundif 5050 tfr2b 7537 rdgfun 7557 oeoa 7722 oeoe 7724 ssdomg 8043 ordtypelem4 8467 ordtypelem6 8469 ordtypelem7 8470 r1limg 8672 rankwflemb 8694 r1elssi 8706 infxpenlem 8874 ackbij2 9103 wunom 9580 mulnzcnopr 10711 negiso 11041 infrenegsup 11044 hashunlei 13250 hashsslei 13251 cos01bnd 14960 cos1bnd 14961 cos2bnd 14962 sin4lt0 14969 egt2lt3 14978 epos 14979 ene1 14982 divalglem5 15167 bitsf1o 15214 gcdaddmlem 15292 strlemor1OLD 16016 zrhpsgnmhm 19978 resubgval 20003 re1r 20007 redvr 20011 refld 20013 txindis 21485 icopnfhmeo 22789 iccpnfcnv 22790 iccpnfhmeo 22791 xrhmeo 22792 cnheiborlem 22800 recvs 22992 qcvs 22993 rrxcph 23226 volf 23343 i1f1 23502 itg11 23503 dvsin 23790 taylthlem2 24173 reefgim 24249 pilem3 24252 pigt2lt4 24253 pire 24255 pipos 24257 sinhalfpi 24265 tan4thpi 24311 sincos3rdpi 24313 circgrp 24343 circsubm 24344 rzgrp 24345 1cubrlem 24613 1cubr 24614 jensenlem2 24759 amgmlem 24761 emcllem6 24772 emcllem7 24773 emgt0 24778 harmonicbnd3 24779 ppiublem1 24972 chtub 24982 bposlem7 25060 lgsdir2lem4 25098 lgsdir2lem5 25099 chebbnd1 25206 mulog2sumlem2 25269 pntpbnd1a 25319 pntpbnd2 25321 pntlemb 25331 pntlemk 25340 qrng0 25355 qrng1 25356 qrngneg 25357 qrngdiv 25358 qabsabv 25363 ex-sqrt 27441 normlem7tALT 28104 hhsssh 28254 shintcli 28316 chintcli 28318 omlsi 28391 qlaxr3i 28623 lnophm 29006 nmcopex 29016 nmcoplb 29017 nmbdfnlbi 29036 nmcfnex 29040 nmcfnlb 29041 hmopidmch 29140 hmopidmpj 29141 chirred 29382 threehalves 29751 nn0archi 29971 xrge0iifiso 30109 xrge0iifmhm 30113 xrge0pluscn 30114 rezh 30143 qqh0 30156 qqh1 30157 qqhcn 30163 qqhucn 30164 rerrext 30181 cnrrext 30182 mbfmvolf 30456 hgt750lem 30857 subfacval3 31297 erdszelem5 31303 erdszelem8 31306 filnetlem3 32500 filnetlem4 32501 bj-genr 32716 bj-genl 32717 bj-genan 32718 pigt3 33532 reheibor 33768 cossssid 34357 fourierdlem68 40709 fourierdlem77 40718 fourierdlem80 40721 fouriersw 40766 etransclem23 40792 gsumge0cl 40906 abcdta 41413 abcdtb 41414 abcdtc 41415 nabctnabc 41419 zlmodzxzsubm 42462 zlmodzxzldeplem3 42616 ldepsnlinclem1 42619 ldepsnlinclem2 42620 ldepsnlinc 42622 empty-surprise 42856 amgmwlem 42876 amgmlemALT 42877 |
Copyright terms: Public domain | W3C validator |