![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exp4a | Structured version Visualization version GIF version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2021.) |
Ref | Expression |
---|---|
exp4a.1 | ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) |
Ref | Expression |
---|---|
exp4a | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp4a.1 | . . 3 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) | |
2 | 1 | imp 444 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | exp4b 633 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 |
This theorem is referenced by: exp4bOLD 636 exp4d 638 exp45 643 exp5c 645 tz7.7 5910 wfrlem12 7595 tfr3 7664 oaass 7810 omordi 7815 nnmordi 7880 fiint 8402 zorn2lem6 9515 zorn2lem7 9516 mulgt0sr 10118 sqlecan 13165 rexuzre 14291 caurcvg 14606 ndvdssub 15335 lsmcv 19343 iscnp4 21269 nrmsep3 21361 2ndcdisj 21461 2ndcsep 21464 tsmsxp 22159 metcnp3 22546 xrlimcnp 24894 ax5seglem5 26012 elspansn4 28741 hoadddir 28972 atcvatlem 29553 sumdmdii 29583 sumdmdlem 29586 isbasisrelowllem1 33514 isbasisrelowllem2 33515 prtlem17 34665 cvratlem 35210 athgt 35245 lplnnle2at 35330 lplncvrlvol2 35404 cdlemb 35583 dalaw 35675 cdleme50trn2 36341 cdlemg18b 36469 dihmeetlem3N 37096 onfrALTlem2 39263 in3an 39338 lindslinindsimp1 42756 |
Copyright terms: Public domain | W3C validator |