Theorem exp4b 430

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  exp4a  431  exp43  436  somo  5600  tz7.7  6378  f1oweALT  7971  soseq  8158  onfununi  8355  odi  8591  omeu  8597  nndi  8635  inf3lem2  9643  axdc3lem2  10465  genpnmax  11021  mulclprlem  11033  distrlem5pr  11041  reclem4pr  11064  lemul12a  12099  sup2  12198  nnmulcl  12264  zbtwnre  12962  elfz0fzfz0  13650  fzofzim  13726  fzo1fzo0n0  13731  elincfzoext  13739  elfzodifsumelfzo  13747  le2sq2  14153  expnbnd  14250  swrdswrd  14723  swrdccat3blem  14757  climbdd  15688  dvdslegcd  16523  oddprmgt2  16718  unbenlem  16928  infpnlem1  16930  prmgaplem6  17076  lmodvsdi  20842  lspsolvlem  21103  lbsextlem2  21120  gsummoncoe1  22246  cpmatmcllem  22656  mp2pm2mplem4  22747  1stccnp  23400  itg2le  25692  ewlkle  29585  clwlkclwwlklem2a  29979  3vfriswmgr  30259  frgrwopreg  30304  frgr2wwlk1  30310  frgrreg  30375  spansneleq  31551  elspansn4  31554  cvmdi  32305  atcvat3i  32377  mdsymlem3  32386  slmdvsdi  33212  satfv0  35380  satffunlem1lem1  35424  satffunlem2lem1  35426  mclsppslem  35605  dfon2lem8  35808  heicant  37679  areacirclem1  37732  areacirclem2  37733  areacirclem4  37735  areacirc  37737  fzmul  37765  cvlexch1  39346  hlrelat2  39422  cvrat3  39461  snatpsubN  39769  pmaple  39780  sn-sup2  42514  fzopredsuc  47352  gbegt5  47775