![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exp4b | Structured version Visualization version GIF version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 430. (Revised by Wolf Lammen, 20-Jul-2021.) |
Ref | Expression |
---|---|
exp4b.1 | ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
Ref | Expression |
---|---|
exp4b | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp4b.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) | |
2 | 1 | expd 414 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏))) |
3 | 2 | ex 411 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: exp4a 430 exp43 435 somo 5627 tz7.7 6397 f1oweALT 7977 soseq 8164 onfununi 8362 odi 8600 omeu 8606 nndi 8644 inf3lem2 9659 axdc3lem2 10481 genpnmax 11037 mulclprlem 11049 distrlem5pr 11057 reclem4pr 11080 lemul12a 12110 sup2 12208 nnmulcl 12274 zbtwnre 12968 elfz0fzfz0 13646 fzofzim 13719 fzo1fzo0n0 13723 elincfzoext 13730 elfzodifsumelfzo 13738 le2sq2 14140 expnbnd 14235 swrdswrd 14696 swrdccat3blem 14730 climbdd 15659 dvdslegcd 16487 oddprmgt2 16678 unbenlem 16885 infpnlem1 16887 prmgaplem6 17033 lmodvsdi 20785 lspsolvlem 21047 lbsextlem2 21064 gsummoncoe1 22257 cpmatmcllem 22669 mp2pm2mplem4 22760 1stccnp 23415 itg2le 25718 ewlkle 29496 clwlkclwwlklem2a 29885 3vfriswmgr 30165 frgrwopreg 30210 frgr2wwlk1 30216 frgrreg 30281 spansneleq 31457 elspansn4 31460 cvmdi 32211 atcvat3i 32283 mdsymlem3 32292 slmdvsdi 33019 satfv0 35101 satffunlem1lem1 35145 satffunlem2lem1 35147 mclsppslem 35326 dfon2lem8 35519 heicant 37261 areacirclem1 37314 areacirclem2 37315 areacirclem4 37317 areacirc 37319 fzmul 37347 cvlexch1 38932 hlrelat2 39008 cvrat3 39047 snatpsubN 39355 pmaple 39366 sn-sup2 42161 fzopredsuc 46843 gbegt5 47240 |
Copyright terms: Public domain | W3C validator |