Theorem exp4b 436

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp4a  437  exp43  442  somo  5606  tz7.7  6387  f1oweALT  7973  soseq  8161  onfununi  8334  odi  8570  omeu  8576  nndi  8615  inf3lem2  9612  axdc3lem2  10457  genpnmax  11020  mulclprlem  11032  distrlem5pr  11040  reclem4pr  11063  lemul12a  12101  sup2  12199  nnmulcl  12285  zbtwnre  12999  elfz0fzfz0  13692  fzofzim  13769  fzo1fzo0n0  13775  elincfzoext  13783  elfzodifsumelfzo  13791  le2sq2  14203  expnbnd  14300  swrdswrd  14778  swrdccat3blem  14812  climbdd  15763  dvdslegcd  16600  oddprmgt2  16796  unbenlem  17006  infpnlem1  17008  prmgaplem6  17154  lmodvsdi  21075  lspsolvlem  21335  lbsextlem2  21352  gsummoncoe1  22539  cpmatmcllem  22949  mp2pm2mplem4  23040  1stccnp  23694  itg2le  25973  ewlkle  30073  clwlkclwwlklem2a  30476  3vfriswmgr  30766  frgrwopreg  30811  frgr2wwlk1  30817  frgrreg  30882  spansneleq  32059  elspansn4  32062  cvmdi  32813  atcvat3i  32885  mdsymlem3  32894  slmdvsdi  33663  satfv0  35945  satffunlem1lem1  35989  satffunlem2lem1  35991  mclsppslem  36170  dfon2lem8  36375  heicant  38412  areacirclem1  38465  areacirclem2  38466  areacirclem4  38468  areacirc  38470  fzmul  38499  cvlexch1  40209  hlrelat2  40284  cvrat3  40323  snatpsubN  40631  pmaple  40642  sn-sup2  43387  fzopredsuc  48220  muldvdsfacgt  48282  muldvdsfacm1  48283  gbegt5  48685