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

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

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  5490  tz7.7  6217  f1oweALT  7723  onfununi  8056  odi  8285  omeu  8291  nndi  8329  inf3lem2  9222  axdc3lem2  10030  genpnmax  10586  mulclprlem  10598  distrlem5pr  10606  reclem4pr  10629  lemul12a  11655  sup2  11753  nnmulcl  11819  zbtwnre  12507  elfz0fzfz0  13182  fzofzim  13254  fzo1fzo0n0  13258  elincfzoext  13265  elfzodifsumelfzo  13273  le2sq2  13671  expnbnd  13764  swrdswrd  14235  swrdccat3blem  14269  climbdd  15200  dvdslegcd  16026  oddprmgt2  16219  unbenlem  16424  infpnlem1  16426  prmgaplem6  16572  lmodvsdi  19876  lspsolvlem  20133  lbsextlem2  20150  gsummoncoe1  21179  cpmatmcllem  21569  mp2pm2mplem4  21660  1stccnp  22313  itg2le  24591  ewlkle  27647  clwlkclwwlklem2a  28035  3vfriswmgr  28315  frgrwopreg  28360  frgr2wwlk1  28366  frgrreg  28431  spansneleq  29605  elspansn4  29608  cvmdi  30359  atcvat3i  30431  mdsymlem3  30440  slmdvsdi  31141  satfv0  32987  satffunlem1lem1  33031  satffunlem2lem1  33033  mclsppslem  33212  dfon2lem8  33436  soseq  33483  heicant  35498  areacirclem1  35551  areacirclem2  35552  areacirclem4  35554  areacirc  35556  fzmul  35585  cvlexch1  37028  hlrelat2  37103  cvrat3  37142  snatpsubN  37450  pmaple  37461  sn-sup2  40088  fzopredsuc  44431  gbegt5  44829