![]() |
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 412 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | 3expd 1352 | 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 206 df-an 396 df-3an 1088 |
This theorem is referenced by: 3anassrs 1359 pm2.61da3ne 3030 po2nr 5602 fliftfund 7313 frfi 9294 fin33i 10370 axdc3lem4 10454 iscatd 17624 isfuncd 17822 isposd 18286 pospropd 18290 imasmnd2 18702 grpinveu 18902 grpid 18903 grpasscan1 18929 imasgrp2 18981 dmdprdd 19917 pgpfac1lem5 19997 imasrng 20078 imasring 20225 islmodd 20708 lmodvsghm 20765 islssd 20778 islmhm2 20882 mulgghm2 21336 isphld 21517 psrbaglefiOLD 21796 riinopn 22730 ordtbaslem 23012 subbascn 23078 haust1 23176 isnrm2 23182 isnrm3 23183 lmmo 23204 nllyidm 23313 tx1stc 23474 filin 23678 filtop 23679 isfil2 23680 infil 23687 fgfil 23699 isufil2 23732 ufileu 23743 filufint 23744 flimopn 23799 flimrest 23807 isxmetd 24152 met2ndc 24352 icccmplem2 24659 lmmbr 25106 cfil3i 25117 equivcfil 25147 bcthlem5 25176 volfiniun 25396 dvidlem 25764 ulmdvlem3 26253 ax5seg 28629 axcontlem4 28658 axcont 28667 grporcan 30204 grpoinveu 30205 grpoid 30206 cvxpconn 34697 cvxsconn 34698 mclsax 35024 mclsppslem 35038 broutsideof2 35564 nn0prpwlem 35671 fgmin 35719 poimirlem27 36979 poimirlem29 36981 poimirlem31 36983 cntotbnd 37128 heiborlem6 37148 heiborlem10 37152 rngonegmn1l 37273 rngonegmn1r 37274 rngoneglmul 37275 rngonegrmul 37276 crngm23 37334 prnc 37399 pridlc3 37405 dmncan1 37408 lsmsat 38342 eqlkr 38433 llncmp 38857 2at0mat0 38860 llncvrlpln 38893 lplncmp 38897 lplnexllnN 38899 lplncvrlvol 38951 lvolcmp 38952 linepsubN 39087 pmapsub 39103 paddasslem16 39170 pmodlem2 39182 lhp2lt 39336 ltrneq2 39483 cdlemf2 39897 cdlemk34 40245 cdlemn11pre 40545 dihord2pre 40560 onexoegt 42456 |
Copyright terms: Public domain | W3C validator |