![]() |
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 1135 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | ad2antll 727 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: el2xptp0 8041 poxp2 8148 ttrcltr 9741 icodiamlt 15418 psgnunilem2 19462 srgbinom 20183 psgndiflemA 21550 haust1 23300 cnhaus 23302 isreg2 23325 llynlly 23425 restnlly 23430 llyrest 23433 llyidm 23436 nllyidm 23437 cldllycmp 23443 txlly 23584 txnlly 23585 pthaus 23586 txhaus 23595 txkgen 23600 xkohaus 23601 xkococnlem 23607 cmetcaulem 25260 itg2add 25733 ulmdvlem3 26383 nosupprefixmo 27679 noinfprefixmo 27680 nosupno 27682 noinfno 27697 etasslt 27792 scutbdaybnd 27794 scutbdaybnd2 27795 addsproplem6 27937 negsproplem6 27991 mulsproplem13 28078 mulsproplem14 28079 mulsprop 28080 ax5seglem6 28817 fusgrfis 29215 wwlksnextfun 29781 umgr2wlkon 29833 connpconn 34976 cvmlift3lem2 35061 cvmlift3lem8 35067 ifscgr 35771 broutsideof3 35853 unblimceq0 36113 paddasslem10 39432 lhpexle2lem 39612 lhpexle3lem 39614 mpaaeu 42716 stoweidlem35 45561 stoweidlem56 45582 stoweidlem59 45585 |
Copyright terms: Public domain | W3C validator |