| 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 1120 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
| 3 | 2 | impd 410 | 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: 3anidm12 1421 mob 3723 dfss2 3969 eqbrrdva 5880 f1oiso2 7372 frxp 8151 onfununi 8381 smoel2 8403 smoiso2 8409 3ecoptocl 8849 ssfi 9213 f1domfi 9221 rex2dom 9282 fodomfib 9369 dffi2 9463 elfiun 9470 dif1card 10050 infxpenlem 10053 cfeq0 10296 cfsuc 10297 cfflb 10299 cfslb2n 10308 cofsmo 10309 domtriomlem 10482 axdc3lem4 10493 axdc4lem 10495 ttukey2g 10556 tskxpss 10812 grudomon 10857 elnpi 11028 dedekind 11424 nn0n0n1ge2b 12595 fzind 12716 suprzcl2 12980 icoshft 13513 fzen 13581 hashgt23el 14463 hashfundm 14481 hashbclem 14491 seqcoll 14503 relexpsucl 15070 relexpsucr 15071 relexpfld 15088 shftuz 15108 mulgcd 16585 algcvga 16616 lcmneg 16640 ressbas 17280 ressbasOLD 17281 resseqnbas 17287 resslemOLD 17288 ressress 17293 psss 18625 tsrlemax 18631 isnmgm 18657 gsummgmpropd 18694 issgrpd 18743 iscmnd 19812 ring1ne0 20296 unitmulclb 20381 isdrngd 20765 isdrngdOLD 20767 abvn0b 20837 issrngd 20856 rmodislmodlem 20927 rmodislmod 20928 isphld 21672 mpfaddcl 22129 mpfmulcl 22130 pf1addcl 22357 pf1mulcl 22358 fitop 22906 hausnei2 23361 ordtt1 23387 locfincmp 23534 basqtop 23719 filfi 23867 fgcl 23886 neifil 23888 filuni 23893 cnextcn 24075 prdsmet 24380 blssps 24434 blss 24435 metcnp3 24553 hlhil 25477 volsup2 25640 sincosq1sgn 26540 sincosq2sgn 26541 sincosq3sgn 26542 sincosq4sgn 26543 sinq12ge0 26550 bcmono 27321 iswlkg 29631 umgrwwlks2on 29977 clwlkclwwlkfo 30028 3cyclfrgrrn1 30304 grpodivf 30557 ipf 30732 shintcli 31348 spanuni 31563 adjadj 31955 unopadj2 31957 hmopadj 31958 hmopbdoptHIL 32007 resvsca 33356 resvlem 33357 resvlemOLD 33358 submateq 33808 esumcocn 34081 bnj1379 34844 bnj571 34920 bnj594 34926 bnj580 34927 bnj600 34933 bnj1189 35023 bnj1321 35041 bnj1384 35046 f1resrcmplf1dlem 35100 cplgredgex 35126 cusgr3cyclex 35141 loop1cycl 35142 umgr2cycllem 35145 umgr2cycl 35146 acycgr2v 35155 cusgracyclt3v 35161 climuzcnv 35676 fness 36350 bj-idreseq 37163 bj-imdiridlem 37186 neificl 37760 metf1o 37762 isismty 37808 ismtybndlem 37813 ablo4pnp 37887 divrngcl 37964 keridl 38039 prnc 38074 lsmsatcv 39011 llncvrlpln2 39559 lplncvrlvol2 39617 linepsubN 39754 pmapsub 39770 dalawlem10 39882 dalawlem13 39885 dalawlem14 39886 dalaw 39888 diaf11N 41051 dibf11N 41163 ismrcd1 42709 ismrcd2 42710 mzpincl 42745 mzpadd 42749 mzpmul 42750 pellfundge 42893 imasgim 43112 sqrtcval 43654 stoweidlem2 46017 stoweidlem17 46032 imaelsetpreimafv 47382 opnneir 48804 i0oii 48817 io1ii 48818 |
| Copyright terms: Public domain | W3C validator |