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 1264 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 447 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: 3anidm12 1383 mob 3388 eqbrrdva 5291 fco 6058 f1oiso2 6602 frxp 7287 onfununi 7438 smoel2 7460 smoiso2 7466 3ecoptocl 7839 dffi2 8329 elfiun 8336 dif1card 8833 infxpenlem 8836 cfeq0 9078 cfsuc 9079 cfflb 9081 cfslb2n 9090 cofsmo 9091 domtriomlem 9264 axdc3lem4 9275 axdc4lem 9277 ttukey2g 9338 tskxpss 9594 grudomon 9639 elnpi 9810 dedekind 10200 nn0n0n1ge2b 11359 fzind 11475 suprzcl2 11778 icoshft 12294 fzen 12358 hashbclem 13236 seqcoll 13248 relexpsucr 13769 relexpsucl 13773 relexpfld 13789 shftuz 13809 mulgcd 15265 algcvga 15292 lcmneg 15316 ressbas 15930 resslem 15933 ressress 15938 psss 17214 tsrlemax 17220 isnmgm 17246 gsummgmpropd 17275 iscmnd 18205 ring1ne0 18591 unitmulclb 18665 isdrngd 18772 issrngd 18861 rmodislmodlem 18930 rmodislmod 18931 abvn0b 19302 mpfaddcl 19534 mpfmulcl 19535 pf1addcl 19717 pf1mulcl 19718 isphld 19999 fitop 20705 hausnei2 21157 ordtt1 21183 locfincmp 21329 basqtop 21514 filfi 21663 fgcl 21682 neifil 21684 filuni 21689 cnextcn 21871 prdsmet 22175 blssps 22229 blss 22230 metcnp3 22345 hlhil 23214 volsup2 23373 sincosq1sgn 24250 sincosq2sgn 24251 sincosq3sgn 24252 sincosq4sgn 24253 sinq12ge0 24260 bcmono 25002 iswlkg 26509 umgrwwlks2on 26850 3cyclfrgrrn1 27149 grpodivf 27392 ipf 27568 shintcli 28188 spanuni 28403 adjadj 28795 unopadj2 28797 hmopadj 28798 hmopbdoptHIL 28847 resvsca 29830 resvlem 29831 submateq 29875 esumcocn 30142 bnj1379 30901 bnj571 30976 bnj594 30982 bnj580 30983 bnj600 30989 bnj1189 31077 bnj1321 31095 bnj1384 31100 climuzcnv 31565 fness 32344 neificl 33549 metf1o 33551 isismty 33600 ismtybndlem 33605 ablo4pnp 33679 divrngcl 33756 keridl 33831 prnc 33866 lsmsatcv 34297 llncvrlpln2 34843 lplncvrlvol2 34901 linepsubN 35038 pmapsub 35054 dalawlem10 35166 dalawlem13 35169 dalawlem14 35170 dalaw 35172 diaf11N 36338 dibf11N 36450 ismrcd1 37261 ismrcd2 37262 mzpincl 37297 mzpadd 37301 mzpmul 37302 pellfundge 37446 imasgim 37670 stoweidlem2 40219 stoweidlem17 40234 |
Copyright terms: Public domain | W3C validator |