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 | id 22 | . 2 ⊢ (𝜓 → 𝜓) | |
2 | 1 | ad5antlr 732 | 1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 397 |
This theorem is referenced by: catcocl 17405 catass 17406 monpropd 17460 subccocl 17571 funcco 17597 funcpropd 17627 mhmmnd 18708 pm2mpmhmlem2 21979 neitr 22342 restutopopn 23401 ustuqtop4 23407 utopreg 23415 cfilucfil 23726 psmetutop 23734 dyadmax 24773 2sqmo 26596 tgifscgr 26880 tgcgrxfr 26890 tgbtwnconn1lem3 26946 tgbtwnconn1 26947 legov 26957 legtrd 26961 legso 26971 miriso 27042 perpneq 27086 footexALT 27090 footex 27093 colperpex 27105 opphllem 27107 midex 27109 opphl 27126 lnopp2hpgb 27135 trgcopyeu 27178 dfcgra2 27202 inaghl 27217 f1otrg 27243 2ndresdju 30995 nn0xmulclb 31103 omndmul2 31347 psgnfzto1stlem 31376 cyc3genpm 31428 nsgqusf1olem3 31609 elrspunidl 31615 rhmimaidl 31618 rhmpreimaprmidl 31636 mxidlprm 31649 ssmxidl 31651 lbsdiflsp0 31716 qtophaus 31795 locfinreflem 31799 cmpcref 31809 pstmxmet 31856 lmxrge0 31911 esumcst 32040 omssubadd 32276 signstfvneq0 32560 afsval 32660 matunitlindflem1 35782 heicant 35821 sstotbnd2 35941 dffltz 40480 flt4lem7 40505 eldioph2b 40594 diophren 40644 pell1234qrdich 40692 iunconnlem2 42537 limcrecl 43152 limclner 43174 icccncfext 43410 ioodvbdlimc1lem2 43455 ioodvbdlimc2lem 43457 stoweidlem60 43583 fourierdlem51 43680 fourierdlem77 43706 fourierdlem103 43732 fourierdlem104 43733 smfaddlem1 44277 smfmullem3 44306 |
Copyright terms: Public domain | W3C validator |