![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3exp2 | Structured version Visualization version GIF version |
Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Ref | Expression |
---|---|
3exp2.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
3exp2 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp2.1 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) | |
2 | 1 | ex 403 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | 3expd 1466 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1111 |
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 387 df-3an 1113 |
This theorem is referenced by: 3anassrs 1473 pm2.61da3ne 3088 po2nr 5278 predpo 5942 fliftfund 6823 frfi 8480 fin33i 9513 axdc3lem4 9597 relexpaddd 14178 iscatd 16693 isfuncd 16884 isposd 17315 pospropd 17494 imasmnd2 17687 grpinveu 17817 grpid 17818 grpasscan1 17839 imasgrp2 17891 dmdprdd 18759 pgpfac1lem5 18839 imasring 18980 islmodd 19232 lmodvsghm 19287 islssd 19299 islmhm2 19404 psrbaglefi 19740 mulgghm2 20212 isphld 20368 riinopn 21090 ordtbaslem 21370 subbascn 21436 haust1 21534 isnrm2 21540 isnrm3 21541 lmmo 21562 nllyidm 21670 tx1stc 21831 filin 22035 filtop 22036 isfil2 22037 infil 22044 fgfil 22056 isufil2 22089 ufileu 22100 filufint 22101 flimopn 22156 flimrest 22164 isxmetd 22508 met2ndc 22705 icccmplem2 23003 lmmbr 23433 cfil3i 23444 equivcfil 23474 bcthlem5 23503 volfiniun 23720 dvidlem 24085 ulmdvlem3 24562 ax5seg 26244 axcontlem4 26273 axcont 26282 grporcan 27924 grpoinveu 27925 grpoid 27926 cvxpconn 31766 cvxsconn 31767 mclsax 32008 mclsppslem 32022 broutsideof2 32763 nn0prpwlem 32850 fgmin 32898 poimirlem27 33975 poimirlem29 33977 poimirlem31 33979 cntotbnd 34132 heiborlem6 34152 heiborlem10 34156 rngonegmn1l 34277 rngonegmn1r 34278 rngoneglmul 34279 rngonegrmul 34280 crngm23 34338 prnc 34403 pridlc3 34409 dmncan1 34412 lsmsat 35078 eqlkr 35169 llncmp 35592 2at0mat0 35595 llncvrlpln 35628 lplncmp 35632 lplnexllnN 35634 lplncvrlvol 35686 lvolcmp 35687 linepsubN 35822 pmapsub 35838 paddasslem16 35905 pmodlem2 35917 lhp2lt 36071 ltrneq2 36218 cdlemf2 36632 cdlemk34 36980 cdlemn11pre 37280 dihord2pre 37295 |
Copyright terms: Public domain | W3C validator |