![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp-5r | Structured version Visualization version GIF version |
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
Ref | Expression |
---|---|
simp-5r | ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 478 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
2 | 1 | ad4antr 725 | 1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 |
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 199 df-an 386 |
This theorem is referenced by: simp-6rOLD 813 catcocl 16657 catass 16658 monpropd 16708 subccocl 16816 funcco 16842 funcpropd 16871 mhmmnd 17850 pm2mpmhmlem2 20949 neitr 21310 restutopopn 22367 ustuqtop4 22373 utopreg 22381 cfilucfil 22689 psmetutop 22697 dyadmax 23703 tgifscgr 25752 tgcgrxfr 25762 tgbtwnconn1lem3 25818 tgbtwnconn1 25819 legov 25829 legtrd 25833 legso 25843 miriso 25914 perpneq 25958 footex 25962 colperpex 25974 opphllem 25976 midex 25978 opphl 25995 lnopp2hpgb 26004 trgcopyeu 26047 dfcgra2 26070 inaghl 26080 f1otrg 26100 clwlksfclwwlkOLD 27395 2sqmo 30157 omndmul2 30220 psgnfzto1stlem 30358 qtophaus 30411 locfinreflem 30415 cmpcref 30425 pstmxmet 30448 lmxrge0 30506 esumcst 30633 omssubadd 30870 signstfvneq0 31160 afsval 31261 matunitlindflem1 33886 heicant 33925 sstotbnd2 34052 eldioph2b 38100 diophren 38151 pell1234qrdich 38199 iunconnlem2 39919 limcrecl 40593 limclner 40615 icccncfext 40832 ioodvbdlimc1lem2 40879 ioodvbdlimc2lem 40881 stoweidlem60 41008 fourierdlem51 41105 fourierdlem77 41131 fourierdlem103 41157 fourierdlem104 41158 smfaddlem1 41705 smfmullem3 41734 |
Copyright terms: Public domain | W3C validator |