Theorem com34 92

Description: Commutation of antecedents. Swap 3rd and 4th. Deduction associated with com23 87. Double deduction associated with com12 33. (Contributed by NM, 25-Apr-1994.)

Hypothesis

Ref	Expression
com4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
com34	⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

Proof of Theorem com34

Step	Hyp	Ref	Expression
1		com4.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2		pm2.04 91	. 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏)))
3	1, 2	syl6 36	1 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4l  93  com35  99  3an1rs  1378  rspct  3563  po2nr  5573  wefrc  5645  tz7.7  6381  funssres  6576  isomin  7337  f1ocnv2d  7666  onint  7793  f1oweALT  7973  bropfvvvv  8092  tfrlem9  8377  tz7.49  8439  oelim  8526  oaordex  8550  omordi  8558  omass  8572  oen0  8579  nnmass  8617  nnmordi  8624  inf3lem2  9614  epfrs  9716  indcardi  10101  ackbij1lem16  10293  cfcoflem  10331  axcc3  10497  zorn2lem7  10561  grur1a  10885  genpcd  11072  genpnmax  11073  mulclprlem  11085  distrlem1pr  11091  ltaddpr  11100  ltexprlem6  11107  ltexprlem7  11108  mulgt0sr  11171  divgt0  12166  divge0  12167  sup2  12254  uzind2  12773  uzwo  13019  supxrun  13427  expnbnd  14356  facdiv  14411  hashimarni  14566  swrdswrdlem  14833  wrd2ind  14852  s3iunsndisj  15101  caubnd  15506  dvdsabseq  16463  lcmfunsnlem2lem1  16793  divgcdcoprm0  16820  ncoprmlnprm  16884  cshwshashlem1  17253  psgnunilem4  19691  lmodvsdi  21140  xrsdsreclblem  21699  nzerooringczr  21766  cpmatacl  23014  riinopn  23206  0ntr  23369  elcls  23371  hausnei2  23651  fgfil  24174  alexsubALTlem2  24347  alexsubALT  24350  aalioulem3  26643  aalioulem4  26644  wilthlem3  27379  2sqreultlem  27756  2sqreunnltlem  27759  bdayfinbndlem1  28835  finsumvtxdg2size  30113  upgrewlkle2  30169  upgrwlkdvdelem  30304  uhgrwkspthlem2  30322  clwwlkinwwlk  30613  wwlksext2clwwlk  30630  1pthon2v  30736  n4cyclfrgr  30874  frgrnbnb  30876  frgrwopreglem4a  30893  frgrreg  30977  frgrregord013  30978  grpoidinvlem3  31090  elspansn5  32158  atcv1  32964  atcvatlem  32969  chirredlem3  32976  mdsymlem3  32989  mdsymlem5  32991  mdsymlem6  32992  sumdmdlem2  33003  f1o3d  33202  slmdvsdi  33758  satfv0fun  36105  satffunlem1lem1  36136  satffunlem2lem1  36138  fgmin  37128  nndivsub  37215  mblfinlem3  38545  rngonegrmul  38846  crngm23  38904  hlrelat2  40428  pmaple  40786  pmodlem2  40872  dalaw  40911  sn-sup2  43523  syl5imp  45454  com3rgbi  45456  ee223  45576  relpmin  45894  2tceilhalfelfzo1  48350  iccpartigtl  48449  iccelpart  48459  lighneallem3  48636  bgoldbtbndlem3  48849  uhgrimisgrgric  48973  clnbgrgrim  48976  clnbgr3stgrgrlic  49062  gpgusgralem  49098  gpgvtxedg0  49105  gpgvtxedg1  49106  ply1mulgsumlem1  49442  fllog2  49624