![]() |
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 407 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | exp4b 431 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: exp4d 434 exp45 439 exp5c 445 tz7.7 6379 wfrlem12OLD 8302 tfr3 8381 oaass 8544 omordi 8549 nnmordi 8614 fiint 9307 zorn2lem6 10478 zorn2lem7 10479 mulgt0sr 11082 sqlecan 14155 rexuzre 15281 caurcvg 15605 ndvdssub 16334 lsmcv 20703 iscnp4 22696 nrmsep3 22788 2ndcdisj 22889 2ndcsep 22892 tsmsxp 23588 metcnp3 23978 xrlimcnp 26400 ax5seglem5 28056 elspansn4 30689 hoadddir 30920 atcvatlem 31501 sumdmdii 31531 sumdmdlem 31534 isbasisrelowllem1 36040 isbasisrelowllem2 36041 disjlem17 37474 prtlem17 37551 cvratlem 38097 athgt 38132 lplnnle2at 38217 lplncvrlvol2 38291 cdlemb 38470 dalaw 38562 cdleme50trn2 39227 cdlemg18b 39355 dihmeetlem3N 39981 onfrALTlem2 43078 in3an 43143 lindslinindsimp1 46786 |
Copyright terms: Public domain | W3C validator |