Theorem exp4b 431

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.)

Hypothesis

Ref	Expression
exp4b.1	⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))

Assertion

Ref	Expression
exp4b	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem exp4b

Step	Hyp	Ref	Expression
1		exp4b.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
2	1	expd 416	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	ex 413	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

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