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 208 df-an 397 |
This theorem is referenced by: exp4d 434 exp45 439 exp5c 445 tz7.7 6210 wfrlem12 7955 tfr3 8024 oaass 8176 omordi 8181 nnmordi 8246 fiint 8783 zorn2lem6 9911 zorn2lem7 9912 mulgt0sr 10515 sqlecan 13559 rexuzre 14700 caurcvg 15021 ndvdssub 15748 lsmcv 19842 iscnp4 21799 nrmsep3 21891 2ndcdisj 21992 2ndcsep 21995 tsmsxp 22690 metcnp3 23077 xrlimcnp 25473 ax5seglem5 26646 elspansn4 29277 hoadddir 29508 atcvatlem 30089 sumdmdii 30119 sumdmdlem 30122 isbasisrelowllem1 34518 isbasisrelowllem2 34519 prtlem17 35892 cvratlem 36437 athgt 36472 lplnnle2at 36557 lplncvrlvol2 36631 cdlemb 36810 dalaw 36902 cdleme50trn2 37567 cdlemg18b 37695 dihmeetlem3N 38321 onfrALTlem2 40757 in3an 40822 lindslinindsimp1 44440 |
Copyright terms: Public domain | W3C validator |