Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3expib | Structured version Visualization version GIF version |
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3expib | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3exp 1256 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 446 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: 3anidm12 1375 mob 3355 eqbrrdva 5213 fco 5971 f1oiso2 6502 frxp 7174 onfununi 7325 smoel2 7347 smoiso2 7353 3ecoptocl 7726 dffi2 8212 elfiun 8219 dif1card 8716 infxpenlem 8719 cfeq0 8961 cfsuc 8962 cfflb 8964 cfslb2n 8973 cofsmo 8974 domtriomlem 9147 axdc3lem4 9158 axdc4lem 9160 ttukey2g 9221 tskxpss 9473 grudomon 9518 elnpi 9689 dedekind 10079 nn0n0n1ge2b 11236 fzind 11351 suprzcl2 11654 icoshft 12165 fzen 12229 hashbclem 13093 seqcoll 13105 relexpsucr 13617 relexpsucl 13621 relexpfld 13637 shftuz 13657 mulgcd 15103 algcvga 15130 lcmneg 15154 ressbas 15757 resslem 15760 ressress 15765 psss 17037 tsrlemax 17043 isnmgm 17069 gsummgmpropd 17098 iscmnd 18028 ring1ne0 18414 unitmulclb 18488 isdrngd 18595 issrngd 18684 abvn0b 19123 mpfaddcl 19355 mpfmulcl 19356 pf1addcl 19538 pf1mulcl 19539 isphld 19818 fitop 20530 hausnei2 20967 ordtt1 20993 locfincmp 21139 basqtop 21324 filfi 21473 fgcl 21492 neifil 21494 filuni 21499 cnextcn 21681 prdsmet 21985 blssps 22039 blss 22040 metcnp3 22155 hlhil 23022 volsup2 23179 sincosq1sgn 24054 sincosq2sgn 24055 sincosq3sgn 24056 sincosq4sgn 24057 sinq12ge0 24064 bcmono 24802 usg2wlkonot 26410 3cyclfrgrarn1 26539 grpodivf 26776 ipf 26952 shintcli 27572 spanuni 27787 adjadj 28179 unopadj2 28181 hmopadj 28182 hmopbdoptHIL 28231 resvsca 29161 resvlem 29162 submateq 29203 esumcocn 29469 bnj1379 30155 bnj571 30230 bnj594 30236 bnj580 30237 bnj600 30243 bnj1189 30331 bnj1321 30349 bnj1384 30354 climuzcnv 30819 fness 31514 neificl 32719 metf1o 32721 isismty 32770 ismtybndlem 32775 ablo4pnp 32849 divrngcl 32926 keridl 33001 prnc 33036 lsmsatcv 33315 llncvrlpln2 33861 lplncvrlvol2 33919 linepsubN 34056 pmapsub 34072 dalawlem10 34184 dalawlem13 34187 dalawlem14 34188 dalaw 34190 diaf11N 35356 dibf11N 35468 ismrcd1 36279 ismrcd2 36280 mzpincl 36315 mzpadd 36319 mzpmul 36320 pellfundge 36464 imasgim 36688 stoweidlem2 38895 stoweidlem17 38910 uhgrauhgrbi 40377 is1wlkg 40816 uspgrn2crct 41011 umgrwwlks2on 41161 3cyclfrgrrn1 41455 |
Copyright terms: Public domain | W3C validator |