Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > expdimp | Structured version Visualization version GIF version |
Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.) |
Ref | Expression |
---|---|
expd.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Ref | Expression |
---|---|
expdimp | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expd.1 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
2 | 1 | expd 452 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp 445 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 |
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 |
This theorem is referenced by: rexlimdvv 3037 ralcom2 3104 ssexnelpss 3720 wereu2 5111 oneqmini 5776 suctr 5808 fun11iun 7126 poxp 7289 suppssr 7326 smoel 7457 omabs 7727 omsmo 7734 iiner 7819 fodomr 8111 fisseneq 8171 suplub2 8367 supnub 8368 infglb 8396 infnlb 8398 inf3lem6 8530 cfcoflem 9094 coftr 9095 zorn2lem7 9324 alephreg 9404 inar1 9597 gruen 9634 letr 10131 lbzbi 11776 xrletr 11989 xmullem 12094 supxrun 12146 ssfzoulel 12562 ssfzo12bi 12563 hashbnd 13123 fi1uzind 13279 brfi1indALT 13282 fi1uzindOLD 13285 brfi1indALTOLD 13288 cau3lem 14094 summo 14448 mertenslem2 14617 prodmolem2 14665 alzdvds 15042 nno 15098 nn0seqcvgd 15283 lcmdvds 15321 lcmf 15346 divgcdodd 15422 prmpwdvds 15608 catpropd 16369 pltnle 16966 pltval3 16967 pltletr 16971 tsrlemax 17220 frgpnabllem1 18276 cyggexb 18300 abvn0b 19302 isphld 19999 indistopon 20805 restntr 20986 cnprest 21093 lmss 21102 lmmo 21184 2ndcdisj 21259 txlm 21451 flftg 21800 bndth 22757 iscmet3 23091 bcthlem5 23125 ovolicc2lem4 23288 ellimc3 23643 lhop1 23777 ulmcaulem 24148 ulmcau 24149 ulmcn 24153 xrlimcnp 24695 ax5seglem4 25812 axcontlem2 25845 axcontlem4 25847 incistruhgr 25974 nbuhgr 26239 uhgrnbgr0nb 26250 wwlknp 26734 wwlksnred 26787 clwlkclwwlklem2a 26899 vdgn0frgrv2 27159 nmcvcn 27550 htthlem 27774 atcvat3i 29255 sumdmdlem2 29278 ifeqeqx 29361 bnj23 30784 bnj849 30995 sotr3 31656 funbreq 31668 nosepssdm 31836 cgrdegen 32111 lineext 32183 btwnconn1lem7 32200 btwnconn1lem14 32207 waj-ax 32413 lukshef-ax2 32414 relowlssretop 33211 finxpreclem6 33233 fin2solem 33395 poimirlem2 33411 poimirlem18 33427 poimirlem21 33430 poimirlem26 33435 poimirlem27 33436 poimirlem31 33440 unirep 33507 seqpo 33543 ssbnd 33587 intidl 33828 prnc 33866 prtlem15 34160 lshpkrlem6 34402 atlatmstc 34606 cvrat3 34728 ps-2 34764 2lplnj 34906 paddasslem5 35110 dochkrshp4 36678 isnacs3 37273 pm14.24 38633 rexlim2d 39857 iccpartigtl 41359 icceuelpartlem 41371 rngcinv 41981 rngcinvALTV 41993 ringcinv 42032 ringcinvALTV 42056 lindslinindsimp1 42246 lindslinindsimp2 42252 digexp 42401 aacllem 42547 |
Copyright terms: Public domain | W3C validator |