![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > simp1bi | Structured version Unicode version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
3simp1bi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
simp1bi |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1bi.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 194 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | simp1d 1000 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 185 df-an 371 df-3an 967 |
This theorem is referenced by: limord 4885 smores2 6924 smofvon2 6926 smofvon 6929 errel 7219 lincmb01cmp 11544 iccf1o 11545 elfznn0 11597 elfzouz 11673 ef01bndlem 13585 sin01bnd 13586 cos01bnd 13587 sin01gt0 13591 cos01gt0 13592 sin02gt0 13593 smueqlem 13803 gzcn 14110 mresspw 14648 drsprs 15224 ipodrscl 15450 subgrcl 15804 pmtrfconj 16090 pgpprm 16212 slwprm 16228 efgsdmi 16349 efgsrel 16351 efgs1b 16353 efgsp1 16354 efgsres 16355 efgsfo 16356 efgredlema 16357 efgredlemf 16358 efgredlemd 16361 efgredlemc 16362 efgredlem 16364 efgrelexlemb 16367 efgcpbllemb 16372 srgcmn 16731 rnggrp 16772 irredcl 16918 lmodgrp 17077 lssss 17140 phllvec 18182 obsrcl 18272 fclstop 19715 tmdmnd 19777 tgpgrp 19780 trgtgp 19873 tdrgtrg 19878 ust0 19925 ngpgrp 20322 elii1 20638 elii2 20639 icopnfcnv 20645 icopnfhmeo 20646 iccpnfhmeo 20648 xrhmeo 20649 oprpiece1res1 20654 oprpiece1res2 20655 phtpcer 20698 pcoval2 20719 pcoass 20727 clmlmod 20770 cphphl 20821 cphnlm 20822 cphsca 20829 bnnvc 20982 uc1pcl 21747 mon1pcl 21748 sinq12ge0 22102 cosq14ge0 22105 cosord 22120 cos11 22121 recosf1o 22123 resinf1o 22124 efifo 22135 logrncn 22146 atanf 22407 atanneg 22434 efiatan 22439 atanlogaddlem 22440 atanlogadd 22441 atanlogsub 22443 efiatan2 22444 2efiatan 22445 tanatan 22446 areass 22485 dchrvmasumlem2 22879 dchrvmasumiflem1 22882 brbtwn2 23302 ax5seglem1 23325 ax5seglem2 23326 ax5seglem3 23328 ax5seglem5 23330 ax5seglem6 23331 ax5seglem9 23334 ax5seg 23335 axbtwnid 23336 axpaschlem 23337 axpasch 23338 axcontlem2 23362 axcontlem4 23364 axcontlem7 23367 subgores 23942 subgoid 23945 subgoinv 23946 sticl 25770 hstcl 25772 omndmnd 26311 slmdcmn 26365 orngrng 26412 elunitrn 26471 rrextnrg 26574 rrextdrg 26575 eulerpartlemd 26892 eulerpartlemf 26896 eulerpartlemgvv 26902 eulerpartlemgu 26903 eulerpartlemgh 26904 eulerpartlemgs2 26906 eulerpartlemn 26907 locfintop 28719 stoweidlem60 30002 2spotiundisj 30802 bnj564 32053 bnj1366 32140 bnj545 32205 bnj548 32207 bnj558 32212 bnj570 32215 bnj580 32223 bnj929 32246 bnj998 32266 bnj1006 32269 bnj1190 32316 bnj1523 32379 atllat 33268 |
Copyright terms: Public domain | W3C validator |