Theorem com34 91

Description: Commutation of antecedents. Swap 3rd and 4th. Deduction associated with com23 86. Double deduction associated with com12 32. (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 90	. 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏)))
3	1, 2	syl6 35	1 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com4l  92  com35  98  3an1rs  1361  rspct  3564  po2nr  5554  wefrc  5626  tz7.7  6351  funssres  6544  isomin  7293  f1ocnv2d  7621  onint  7745  f1oweALT  7926  bropfvvvv  8044  tfrlem9  8326  tz7.49  8386  oelim  8471  oaordex  8495  omordi  8503  omass  8517  oen0  8524  nnmass  8562  nnmordi  8569  inf3lem2  9550  epfrs  9652  indcardi  9963  ackbij1lem16  10156  cfcoflem  10194  axcc3  10360  zorn2lem7  10424  grur1a  10742  genpcd  10929  genpnmax  10930  mulclprlem  10942  distrlem1pr  10948  ltaddpr  10957  ltexprlem6  10964  ltexprlem7  10965  mulgt0sr  11028  divgt0  12022  divge0  12023  sup2  12110  uzind2  12597  uzwo  12836  supxrun  13243  expnbnd  14167  facdiv  14222  hashimarni  14376  swrdswrdlem  14639  wrd2ind  14658  s3iunsndisj  14903  caubnd  15294  dvdsabseq  16252  lcmfunsnlem2lem1  16577  divgcdcoprm0  16604  ncoprmlnprm  16667  cshwshashlem1  17035  psgnunilem4  19438  lmodvsdi  20848  xrsdsreclblem  21379  nzerooringczr  21447  cpmatacl  22672  riinopn  22864  0ntr  23027  elcls  23029  hausnei2  23309  fgfil  23831  alexsubALTlem2  24004  alexsubALT  24007  aalioulem3  26310  aalioulem4  26311  wilthlem3  27048  2sqreultlem  27426  2sqreunnltlem  27429  bdayfinbndlem1  28475  finsumvtxdg2size  29636  upgrewlkle2  29692  upgrwlkdvdelem  29821  uhgrwkspthlem2  29839  clwwlkinwwlk  30127  wwlksext2clwwlk  30144  1pthon2v  30240  n4cyclfrgr  30378  frgrnbnb  30380  frgrwopreglem4a  30397  frgrreg  30481  frgrregord013  30482  grpoidinvlem3  30593  elspansn5  31661  atcv1  32467  atcvatlem  32472  chirredlem3  32479  mdsymlem3  32492  mdsymlem5  32494  mdsymlem6  32495  sumdmdlem2  32506  f1o3d  32715  slmdvsdi  33308  satfv0fun  35584  satffunlem1lem1  35615  satffunlem2lem1  35617  fgmin  36583  nndivsub  36670  mblfinlem3  37907  rngonegrmul  38192  crngm23  38250  hlrelat2  39776  pmaple  40134  pmodlem2  40220  dalaw  40259  sn-sup2  42858  syl5imp  44865  com3rgbi  44867  ee223  44987  relpmin  45305  2tceilhalfelfzo1  47689  iccpartigtl  47780  iccelpart  47790  lighneallem3  47964  bgoldbtbndlem3  48164  uhgrimisgrgric  48288  clnbgrgrim  48291  clnbgr3stgrgrlic  48377  gpgusgralem  48413  gpgvtxedg0  48420  gpgvtxedg1  48421  ply1mulgsumlem1  48743  fllog2  48925