Theorem exp4b 435

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  exp4a  436  exp43  441  somo  5610  tz7.7  6388  f1oweALT  7970  soseq  8156  onfununi  8329  odi  8565  omeu  8571  nndi  8610  inf3lem2  9599  axdc3lem2  10436  genpnmax  10993  mulclprlem  11005  distrlem5pr  11013  reclem4pr  11036  lemul12a  12074  sup2  12172  nnmulcl  12258  zbtwnre  12971  elfz0fzfz0  13663  fzofzim  13740  fzo1fzo0n0  13746  elincfzoext  13754  elfzodifsumelfzo  13762  le2sq2  14173  expnbnd  14270  swrdswrd  14744  swrdccat3blem  14778  climbdd  15725  dvdslegcd  16563  oddprmgt2  16759  unbenlem  16969  infpnlem1  16971  prmgaplem6  17117  lmodvsdi  20987  lspsolvlem  21247  lbsextlem2  21264  gsummoncoe1  22449  cpmatmcllem  22856  mp2pm2mplem4  22947  1stccnp  23600  itg2le  25879  ewlkle  29933  clwlkclwwlklem2a  30327  3vfriswmgr  30607  frgrwopreg  30652  frgr2wwlk1  30658  frgrreg  30723  spansneleq  31900  elspansn4  31903  cvmdi  32654  atcvat3i  32726  mdsymlem3  32735  slmdvsdi  33513  satfv0  35828  satffunlem1lem1  35872  satffunlem2lem1  35874  mclsppslem  36053  dfon2lem8  36258  heicant  38284  areacirclem1  38337  areacirclem2  38338  areacirclem4  38340  areacirc  38342  fzmul  38370  cvlexch1  40080  hlrelat2  40155  cvrat3  40194  snatpsubN  40502  pmaple  40513  sn-sup2  43243  fzopredsuc  48038  muldvdsfacgt  48100  muldvdsfacm1  48101  gbegt5  48503