| 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 1354 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 1089 |
| This theorem is referenced by: 3anassrs 1361 pm2.61da3ne 3031 po2nr 5606 fliftfund 7333 frfi 9321 fin33i 10409 axdc3lem4 10493 iscatd 17716 isfuncd 17910 isposd 18368 pospropd 18372 imasmnd2 18787 grpinveu 18992 grpid 18993 grpasscan1 19019 imasgrp2 19073 dmdprdd 20019 pgpfac1lem5 20099 imasrng 20174 imasring 20327 islmodd 20864 lmodvsghm 20921 islssd 20933 islmhm2 21037 mulgghm2 21487 isphld 21672 riinopn 22914 ordtbaslem 23196 subbascn 23262 haust1 23360 isnrm2 23366 isnrm3 23367 lmmo 23388 nllyidm 23497 tx1stc 23658 filin 23862 filtop 23863 isfil2 23864 infil 23871 fgfil 23883 isufil2 23916 ufileu 23927 filufint 23928 flimopn 23983 flimrest 23991 isxmetd 24336 met2ndc 24536 icccmplem2 24845 lmmbr 25292 cfil3i 25303 equivcfil 25333 bcthlem5 25362 volfiniun 25582 dvidlem 25950 ulmdvlem3 26445 ax5seg 28953 axcontlem4 28982 axcont 28991 grporcan 30537 grpoinveu 30538 grpoid 30539 cvxpconn 35247 cvxsconn 35248 mclsax 35574 mclsppslem 35588 r1peuqusdeg1 35648 broutsideof2 36123 nn0prpwlem 36323 fgmin 36371 poimirlem27 37654 poimirlem29 37656 poimirlem31 37658 cntotbnd 37803 heiborlem6 37823 heiborlem10 37827 rngonegmn1l 37948 rngonegmn1r 37949 rngoneglmul 37950 rngonegrmul 37951 crngm23 38009 prnc 38074 pridlc3 38080 dmncan1 38083 lsmsat 39009 eqlkr 39100 llncmp 39524 2at0mat0 39527 llncvrlpln 39560 lplncmp 39564 lplnexllnN 39566 lplncvrlvol 39618 lvolcmp 39619 linepsubN 39754 pmapsub 39770 paddasslem16 39837 pmodlem2 39849 lhp2lt 40003 ltrneq2 40150 cdlemf2 40564 cdlemk34 40912 cdlemn11pre 41212 dihord2pre 41227 onexoegt 43256 clnbgrssedg 47827 clnbgrgrimlem 47901 grimgrtri 47916 |
| Copyright terms: Public domain | W3C validator |