|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simprr3 | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) | 
| Ref | Expression | 
|---|---|
| simprr3 | ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simp3 1138 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
| 2 | 1 | ad2antll 729 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 | 
| 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 207 df-an 396 df-3an 1088 | 
| This theorem is referenced by: el2xptp0 8062 poxp2 8169 ttrcltr 9757 icodiamlt 15475 psgnunilem2 19514 srgbinom 20229 psgndiflemA 21620 haust1 23361 cnhaus 23363 isreg2 23386 llynlly 23486 restnlly 23491 llyrest 23494 llyidm 23497 nllyidm 23498 cldllycmp 23504 txlly 23645 txnlly 23646 pthaus 23647 txhaus 23656 txkgen 23661 xkohaus 23662 xkococnlem 23668 cmetcaulem 25323 itg2add 25795 ulmdvlem3 26446 nosupprefixmo 27746 noinfprefixmo 27747 nosupno 27749 noinfno 27764 etasslt 27859 scutbdaybnd 27861 scutbdaybnd2 27862 addsproplem6 28008 negsproplem6 28066 mulsproplem13 28155 mulsproplem14 28156 mulsprop 28157 ax5seglem6 28950 fusgrfis 29348 wwlksnextfun 29919 umgr2wlkon 29971 connpconn 35241 cvmlift3lem2 35326 cvmlift3lem8 35332 ifscgr 36046 broutsideof3 36128 unblimceq0 36509 paddasslem10 39832 lhpexle2lem 40012 lhpexle3lem 40014 mpaaeu 43167 stoweidlem35 46055 stoweidlem56 46076 stoweidlem59 46079 | 
| Copyright terms: Public domain | W3C validator |