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  5602  tz7.7  6406  f1oweALT  8008  soseq  8203  onfununi  8377  odi  8615  omeu  8621  nndi  8660  inf3lem2  9657  axdc3lem2  10556  genpnmax  11119  mulclprlem  11131  distrlem5pr  11139  reclem4pr  11162  lemul12a  12202  sup2  12300  nnmulcl  12386  zbtwnre  13100  elfz0fzfz0  13794  fzofzim  13871  fzo1fzo0n0  13877  elincfzoext  13885  elfzodifsumelfzo  13893  le2sq2  14305  expnbnd  14403  swrdswrd  14882  swrdccat3blem  14916  climbdd  15868  dvdslegcd  16703  oddprmgt2  16904  unbenlem  17115  infpnlem1  17117  prmgaplem6  17263  lmodvsdi  21190  lspsolvlem  21450  lbsextlem2  21467  gsummoncoe1  22656  cpmatmcllem  23066  mp2pm2mplem4  23157  1stccnp  23811  itg2le  26090  ewlkle  30216  clwlkclwwlklem2a  30619  3vfriswmgr  30909  frgrwopreg  30954  frgr2wwlk1  30960  frgrreg  31025  spansneleq  32202  elspansn4  32205  cvmdi  32956  atcvat3i  33028  mdsymlem3  33037  slmdvsdi  33846  satfv0  36290  satffunlem1lem1  36334  satffunlem2lem1  36336  mclsppslem  36515  dfon2lem8  36730  heicant  38765  areacirclem1  38818  areacirclem2  38819  areacirclem4  38821  areacirc  38823  fzmul  38867  cvlexch1  40577  hlrelat2  40652  cvrat3  40691  snatpsubN  40999  pmaple  41010  sn-sup2  43748  fzopredsuc  48599  muldvdsfacgt  48661  muldvdsfacm1  48662  gbegt5  49064