Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp4b Structured version   Visualization version   GIF version

Theorem exp4b 434
 Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 435. (Revised by Wolf Lammen, 20-Jul-2021.)
Hypothesis
Ref Expression
exp4b.1 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
Assertion
Ref Expression
exp4b (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem exp4b
StepHypRef Expression
1 exp4b.1 . . 3 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
21expd 419 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32ex 416 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  exp4a  435  exp43  440  somo  5478  tz7.7  6189  f1oweALT  7659  onfununi  7965  odi  8192  omeu  8198  nndi  8236  inf3lem2  9080  axdc3lem2  9866  genpnmax  10422  mulclprlem  10434  distrlem5pr  10442  reclem4pr  10465  lemul12a  11491  sup2  11588  nnmulcl  11653  zbtwnre  12338  elfz0fzfz0  13011  fzofzim  13083  fzo1fzo0n0  13087  elincfzoext  13094  elfzodifsumelfzo  13102  le2sq2  13500  expnbnd  13593  swrdswrd  14062  swrdccat3blem  14096  climbdd  15023  dvdslegcd  15846  oddprmgt2  16036  unbenlem  16237  infpnlem1  16239  prmgaplem6  16385  lmodvsdi  19653  lspsolvlem  19910  lbsextlem2  19927  gsummoncoe1  20936  cpmatmcllem  21326  mp2pm2mplem4  21417  1stccnp  22070  itg2le  24346  ewlkle  27398  clwlkclwwlklem2a  27786  3vfriswmgr  28066  frgrwopreg  28111  frgr2wwlk1  28117  frgrreg  28182  spansneleq  29356  elspansn4  29359  cvmdi  30110  atcvat3i  30182  mdsymlem3  30191  slmdvsdi  30896  satfv0  32713  satffunlem1lem1  32757  satffunlem2lem1  32759  mclsppslem  32938  dfon2lem8  33143  soseq  33204  heicant  35085  areacirclem1  35138  areacirclem2  35139  areacirclem4  35141  areacirc  35143  fzmul  35172  cvlexch1  36617  hlrelat2  36692  cvrat3  36731  snatpsubN  37039  pmaple  37050  sn-sup2  39581  fzopredsuc  43867  gbegt5  44266
 Copyright terms: Public domain W3C validator