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  5570  tz7.7  6337  f1oweALT  7914  soseq  8099  onfununi  8271  odi  8504  omeu  8510  nndi  8548  inf3lem2  9544  axdc3lem2  10364  genpnmax  10920  mulclprlem  10932  distrlem5pr  10940  reclem4pr  10963  lemul12a  12000  sup2  12099  nnmulcl  12170  zbtwnre  12865  elfz0fzfz0  13554  fzofzim  13630  fzo1fzo0n0  13636  elincfzoext  13644  elfzodifsumelfzo  13652  le2sq2  14060  expnbnd  14157  swrdswrd  14629  swrdccat3blem  14663  climbdd  15597  dvdslegcd  16433  oddprmgt2  16628  unbenlem  16838  infpnlem1  16840  prmgaplem6  16986  lmodvsdi  20806  lspsolvlem  21067  lbsextlem2  21084  gsummoncoe1  22211  cpmatmcllem  22621  mp2pm2mplem4  22712  1stccnp  23365  itg2le  25656  ewlkle  29569  clwlkclwwlklem2a  29960  3vfriswmgr  30240  frgrwopreg  30285  frgr2wwlk1  30291  frgrreg  30356  spansneleq  31532  elspansn4  31535  cvmdi  32286  atcvat3i  32358  mdsymlem3  32367  slmdvsdi  33167  satfv0  35330  satffunlem1lem1  35374  satffunlem2lem1  35376  mclsppslem  35555  dfon2lem8  35763  heicant  37634  areacirclem1  37687  areacirclem2  37688  areacirclem4  37690  areacirc  37692  fzmul  37720  cvlexch1  39306  hlrelat2  39382  cvrat3  39421  snatpsubN  39729  pmaple  39740  sn-sup2  42464  fzopredsuc  47308  gbegt5  47746