|   | 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 406 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) | 
| 3 | 2 | exp4b 430 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: exp4d 433 exp45 438 exp5c 444 tz7.7 6409 wfrlem12OLD 8361 tfr3 8440 oaass 8600 omordi 8605 nnmordi 8670 fiint 9367 fiintOLD 9368 zorn2lem6 10542 zorn2lem7 10543 mulgt0sr 11146 sqlecan 14249 rexuzre 15392 caurcvg 15714 ndvdssub 16447 lsmcv 21144 iscnp4 23272 nrmsep3 23364 2ndcdisj 23465 2ndcsep 23468 tsmsxp 24164 metcnp3 24554 xrlimcnp 27012 ax5seglem5 28949 elspansn4 31593 hoadddir 31824 atcvatlem 32405 sumdmdii 32435 sumdmdlem 32438 isbasisrelowllem1 37357 isbasisrelowllem2 37358 disjlem17 38801 prtlem17 38878 cvratlem 39424 athgt 39459 lplnnle2at 39544 lplncvrlvol2 39618 cdlemb 39797 dalaw 39889 cdleme50trn2 40554 cdlemg18b 40682 dihmeetlem3N 41308 onfrALTlem2 44571 in3an 44636 lindslinindsimp1 48379 | 
| Copyright terms: Public domain | W3C validator |