![]() |
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 432. (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 416 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏))) |
3 | 2 | ex 413 | 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: exp4a 432 exp43 437 somo 5390 tz7.7 6084 f1oweALT 7520 onfununi 7821 odi 8046 omeu 8052 nndi 8090 inf3lem2 8927 axdc3lem2 9708 genpnmax 10264 mulclprlem 10276 distrlem5pr 10284 reclem4pr 10307 lemul12a 11335 sup2 11434 nnmulcl 11498 zbtwnre 12184 elfz0fzfz0 12851 fzofzim 12922 fzo1fzo0n0 12926 elincfzoext 12933 elfzodifsumelfzo 12941 le2sq2 13338 expnbnd 13431 swrdswrd 13891 swrdccat3blem 13925 climbdd 14850 dvdslegcd 15674 oddprmgt2 15860 unbenlem 16061 infpnlem1 16063 prmgaplem6 16209 lmodvsdi 19335 lspsolvlem 19592 lbsextlem2 19609 gsummoncoe1 20143 cpmatmcllem 20998 mp2pm2mplem4 21089 1stccnp 21742 itg2le 24011 ewlkle 27058 clwlkclwwlklem2a 27451 3vfriswmgr 27737 frgrwopreg 27782 frgr2wwlk1 27788 frgrreg 27853 spansneleq 29026 elspansn4 29029 cvmdi 29780 atcvat3i 29852 mdsymlem3 29861 slmdvsdi 30439 satfv0 32169 satffunlem1lem1 32210 satffunlem2lem1 32212 mclsppslem 32383 dfon2lem8 32588 soseq 32650 heicant 34404 areacirclem1 34459 areacirclem2 34460 areacirclem4 34462 areacirc 34464 fzmul 34494 cvlexch1 35945 hlrelat2 36020 cvrat3 36059 snatpsubN 36367 pmaple 36378 fzopredsuc 42993 gbegt5 43362 |
Copyright terms: Public domain | W3C validator |