![]() |
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 1113 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 446 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 385 df-3an 1074 |
This theorem is referenced by: 3anidm12 1530 mob 3529 eqbrrdva 5447 fco 6219 f1oiso2 6766 frxp 7456 onfununi 7608 smoel2 7630 smoiso2 7636 3ecoptocl 8008 dffi2 8496 elfiun 8503 dif1card 9043 infxpenlem 9046 cfeq0 9290 cfsuc 9291 cfflb 9293 cfslb2n 9302 cofsmo 9303 domtriomlem 9476 axdc3lem4 9487 axdc4lem 9489 ttukey2g 9550 tskxpss 9806 grudomon 9851 elnpi 10022 dedekind 10412 nn0n0n1ge2b 11571 fzind 11687 suprzcl2 11991 icoshft 12507 fzen 12571 hashbclem 13448 seqcoll 13460 relexpsucr 13988 relexpsucl 13992 relexpfld 14008 shftuz 14028 mulgcd 15487 algcvga 15514 lcmneg 15538 ressbas 16152 resslem 16155 ressress 16160 psss 17435 tsrlemax 17441 isnmgm 17467 gsummgmpropd 17496 iscmnd 18425 ring1ne0 18811 unitmulclb 18885 isdrngd 18994 issrngd 19083 rmodislmodlem 19152 rmodislmod 19153 abvn0b 19524 mpfaddcl 19756 mpfmulcl 19757 pf1addcl 19939 pf1mulcl 19940 isphld 20221 fitop 20927 hausnei2 21379 ordtt1 21405 locfincmp 21551 basqtop 21736 filfi 21884 fgcl 21903 neifil 21905 filuni 21910 cnextcn 22092 prdsmet 22396 blssps 22450 blss 22451 metcnp3 22566 hlhil 23434 volsup2 23593 sincosq1sgn 24470 sincosq2sgn 24471 sincosq3sgn 24472 sincosq4sgn 24473 sinq12ge0 24480 bcmono 25222 iswlkg 26740 umgrwwlks2on 27099 clwlkclwwlkfo 27153 3cyclfrgrrn1 27460 grpodivf 27722 ipf 27898 shintcli 28518 spanuni 28733 adjadj 29125 unopadj2 29127 hmopadj 29128 hmopbdoptHIL 29177 resvsca 30160 resvlem 30161 submateq 30205 esumcocn 30472 bnj1379 31229 bnj571 31304 bnj594 31310 bnj580 31311 bnj600 31317 bnj1189 31405 bnj1321 31423 bnj1384 31428 climuzcnv 31893 fness 32671 neificl 33880 metf1o 33882 isismty 33931 ismtybndlem 33936 ablo4pnp 34010 divrngcl 34087 keridl 34162 prnc 34197 lsmsatcv 34818 llncvrlpln2 35364 lplncvrlvol2 35422 linepsubN 35559 pmapsub 35575 dalawlem10 35687 dalawlem13 35690 dalawlem14 35691 dalaw 35693 diaf11N 36858 dibf11N 36970 ismrcd1 37781 ismrcd2 37782 mzpincl 37817 mzpadd 37821 mzpmul 37822 pellfundge 37966 imasgim 38190 stoweidlem2 40740 stoweidlem17 40755 |
Copyright terms: Public domain | W3C validator |