| 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 431. (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 415 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏))) |
| 3 | 2 | ex 412 | 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: exp4a 431 exp43 436 somo 5631 tz7.7 6410 f1oweALT 7997 soseq 8184 onfununi 8381 odi 8617 omeu 8623 nndi 8661 inf3lem2 9669 axdc3lem2 10491 genpnmax 11047 mulclprlem 11059 distrlem5pr 11067 reclem4pr 11090 lemul12a 12125 sup2 12224 nnmulcl 12290 zbtwnre 12988 elfz0fzfz0 13673 fzofzim 13749 fzo1fzo0n0 13754 elincfzoext 13762 elfzodifsumelfzo 13770 le2sq2 14175 expnbnd 14271 swrdswrd 14743 swrdccat3blem 14777 climbdd 15708 dvdslegcd 16541 oddprmgt2 16736 unbenlem 16946 infpnlem1 16948 prmgaplem6 17094 lmodvsdi 20883 lspsolvlem 21144 lbsextlem2 21161 gsummoncoe1 22312 cpmatmcllem 22724 mp2pm2mplem4 22815 1stccnp 23470 itg2le 25774 ewlkle 29623 clwlkclwwlklem2a 30017 3vfriswmgr 30297 frgrwopreg 30342 frgr2wwlk1 30348 frgrreg 30413 spansneleq 31589 elspansn4 31592 cvmdi 32343 atcvat3i 32415 mdsymlem3 32424 slmdvsdi 33221 satfv0 35363 satffunlem1lem1 35407 satffunlem2lem1 35409 mclsppslem 35588 dfon2lem8 35791 heicant 37662 areacirclem1 37715 areacirclem2 37716 areacirclem4 37718 areacirc 37720 fzmul 37748 cvlexch1 39329 hlrelat2 39405 cvrat3 39444 snatpsubN 39752 pmaple 39763 sn-sup2 42501 fzopredsuc 47335 gbegt5 47748 |
| Copyright terms: Public domain | W3C validator |