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  5597  tz7.7  6388  f1oweALT  7984  soseq  8178  onfununi  8352  odi  8590  omeu  8596  nndi  8635  inf3lem2  9633  axdc3lem2  10532  genpnmax  11095  mulclprlem  11107  distrlem5pr  11115  reclem4pr  11138  lemul12a  12178  sup2  12276  nnmulcl  12362  zbtwnre  13076  elfz0fzfz0  13770  fzofzim  13847  fzo1fzo0n0  13853  elincfzoext  13861  elfzodifsumelfzo  13869  le2sq2  14281  expnbnd  14379  swrdswrd  14858  swrdccat3blem  14892  climbdd  15844  dvdslegcd  16679  oddprmgt2  16880  unbenlem  17091  infpnlem1  17093  prmgaplem6  17239  lmodvsdi  21165  lspsolvlem  21425  lbsextlem2  21442  gsummoncoe1  22631  cpmatmcllem  23041  mp2pm2mplem4  23132  1stccnp  23786  itg2le  26065  ewlkle  30191  clwlkclwwlklem2a  30594  3vfriswmgr  30884  frgrwopreg  30929  frgr2wwlk1  30935  frgrreg  31000  spansneleq  32177  elspansn4  32180  cvmdi  32931  atcvat3i  33003  mdsymlem3  33012  slmdvsdi  33822  satfv0  36209  satffunlem1lem1  36253  satffunlem2lem1  36255  mclsppslem  36434  dfon2lem8  36644  heicant  38666  areacirclem1  38719  areacirclem2  38720  areacirclem4  38722  areacirc  38724  fzmul  38768  cvlexch1  40478  hlrelat2  40553  cvrat3  40592  snatpsubN  40900  pmaple  40911  sn-sup2  43648  fzopredsuc  48487  muldvdsfacgt  48549  muldvdsfacm1  48550  gbegt5  48952