Theorem exp4b 432

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 433. (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 417	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	ex 414	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  exp4a  433  exp43  438  somo  5626  tz7.7  6391  f1oweALT  7959  soseq  8145  onfununi  8341  odi  8579  omeu  8585  nndi  8623  inf3lem2  9624  axdc3lem2  10446  genpnmax  11002  mulclprlem  11014  distrlem5pr  11022  reclem4pr  11045  lemul12a  12072  sup2  12170  nnmulcl  12236  zbtwnre  12930  elfz0fzfz0  13606  fzofzim  13679  fzo1fzo0n0  13683  elincfzoext  13690  elfzodifsumelfzo  13698  le2sq2  14100  expnbnd  14195  swrdswrd  14655  swrdccat3blem  14689  climbdd  15618  dvdslegcd  16445  oddprmgt2  16636  unbenlem  16841  infpnlem1  16843  prmgaplem6  16989  lmodvsdi  20495  lspsolvlem  20755  lbsextlem2  20772  gsummoncoe1  21828  cpmatmcllem  22220  mp2pm2mplem4  22311  1stccnp  22966  itg2le  25257  ewlkle  28862  clwlkclwwlklem2a  29251  3vfriswmgr  29531  frgrwopreg  29576  frgr2wwlk1  29582  frgrreg  29647  spansneleq  30823  elspansn4  30826  cvmdi  31577  atcvat3i  31649  mdsymlem3  31658  slmdvsdi  32360  satfv0  34349  satffunlem1lem1  34393  satffunlem2lem1  34395  mclsppslem  34574  dfon2lem8  34762  heicant  36523  areacirclem1  36576  areacirclem2  36577  areacirclem4  36579  areacirc  36581  fzmul  36609  cvlexch1  38198  hlrelat2  38274  cvrat3  38313  snatpsubN  38621  pmaple  38632  sn-sup2  41342  fzopredsuc  46031  gbegt5  46429