Theorem exp4b 433

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  exp4a  434  exp43  439  somo  5587  tz7.7  6361  f1oweALT  7942  soseq  8127  onfununi  8300  odi  8536  omeu  8542  nndi  8581  inf3lem2  9574  axdc3lem2  10398  genpnmax  10955  mulclprlem  10967  distrlem5pr  10975  reclem4pr  10998  lemul12a  12039  sup2  12138  nnmulcl  12224  zbtwnre  12937  elfz0fzfz0  13628  fzofzim  13705  fzo1fzo0n0  13711  elincfzoext  13719  elfzodifsumelfzo  13727  le2sq2  14138  expnbnd  14235  swrdswrd  14708  swrdccat3blem  14742  climbdd  15675  dvdslegcd  16514  oddprmgt2  16710  unbenlem  16920  infpnlem1  16922  prmgaplem6  17068  lmodvsdi  20925  lspsolvlem  21185  lbsextlem2  21202  gsummoncoe1  22344  cpmatmcllem  22751  mp2pm2mplem4  22842  1stccnp  23495  itg2le  25774  ewlkle  29745  clwlkclwwlklem2a  30139  3vfriswmgr  30419  frgrwopreg  30464  frgr2wwlk1  30470  frgrreg  30535  spansneleq  31712  elspansn4  31715  cvmdi  32466  atcvat3i  32538  mdsymlem3  32547  slmdvsdi  33349  satfv0  35656  satffunlem1lem1  35700  satffunlem2lem1  35702  mclsppslem  35881  dfon2lem8  36086  heicant  38102  areacirclem1  38155  areacirclem2  38156  areacirclem4  38158  areacirc  38160  fzmul  38188  cvlexch1  39900  hlrelat2  39975  cvrat3  40014  snatpsubN  40322  pmaple  40333  sn-sup2  43061  fzopredsuc  47866  muldvdsfacgt  47928  muldvdsfacm1  47929  gbegt5  48331