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 413 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | 3expd 1345 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: 3anassrs 1352 pm2.61da3ne 3103 po2nr 5480 predpo 6159 fliftfund 7055 frfi 8751 fin33i 9779 axdc3lem4 9863 relexpaddd 14401 iscatd 16932 isfuncd 17123 isposd 17553 pospropd 17732 imasmnd2 17936 grpinveu 18076 grpid 18077 grpasscan1 18100 imasgrp2 18152 dmdprdd 19050 pgpfac1lem5 19130 imasring 19298 islmodd 19569 lmodvsghm 19624 islssd 19636 islmhm2 19739 psrbaglefi 20080 mulgghm2 20572 isphld 20726 riinopn 21444 ordtbaslem 21724 subbascn 21790 haust1 21888 isnrm2 21894 isnrm3 21895 lmmo 21916 nllyidm 22025 tx1stc 22186 filin 22390 filtop 22391 isfil2 22392 infil 22399 fgfil 22411 isufil2 22444 ufileu 22455 filufint 22456 flimopn 22511 flimrest 22519 isxmetd 22863 met2ndc 23060 icccmplem2 23358 lmmbr 23788 cfil3i 23799 equivcfil 23829 bcthlem5 23858 volfiniun 24075 dvidlem 24440 ulmdvlem3 24917 ax5seg 26651 axcontlem4 26680 axcont 26689 grporcan 28222 grpoinveu 28223 grpoid 28224 cvxpconn 32386 cvxsconn 32387 mclsax 32713 mclsppslem 32727 broutsideof2 33480 nn0prpwlem 33567 fgmin 33615 poimirlem27 34800 poimirlem29 34802 poimirlem31 34804 cntotbnd 34955 heiborlem6 34975 heiborlem10 34979 rngonegmn1l 35100 rngonegmn1r 35101 rngoneglmul 35102 rngonegrmul 35103 crngm23 35161 prnc 35226 pridlc3 35232 dmncan1 35235 lsmsat 36024 eqlkr 36115 llncmp 36538 2at0mat0 36541 llncvrlpln 36574 lplncmp 36578 lplnexllnN 36580 lplncvrlvol 36632 lvolcmp 36633 linepsubN 36768 pmapsub 36784 paddasslem16 36851 pmodlem2 36863 lhp2lt 37017 ltrneq2 37164 cdlemf2 37578 cdlemk34 37926 cdlemn11pre 38226 dihord2pre 38241 |
Copyright terms: Public domain | W3C validator |