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  3570  po2nr  5588  wefrc  5660  tz7.7  6393  funssres  6587  isomin  7346  f1ocnv2d  7676  onint  7798  f1oweALT  7978  bropfvvvv  8096  tfrlem9  8381  tz7.49  8441  oelim  8528  oaordex  8552  omordi  8560  omass  8574  oen0  8581  nnmass  8619  nnmordi  8626  inf3lem2  9608  epfrs  9710  indcardi  10044  ackbij1lem16  10236  cfcoflem  10274  axcc3  10440  zorn2lem7  10504  grur1a  10822  genpcd  11009  genpnmax  11010  mulclprlem  11022  distrlem1pr  11028  ltaddpr  11037  ltexprlem6  11044  ltexprlem7  11045  mulgt0sr  11108  divgt0  12101  divge0  12102  sup2  12189  uzind2  12707  uzwo  12953  supxrun  13360  expnbnd  14288  facdiv  14343  hashimarni  14498  swrdswrdlem  14765  wrd2ind  14784  s3iunsndisj  15031  caubnd  15436  dvdsabseq  16396  lcmfunsnlem2lem1  16721  divgcdcoprm0  16748  ncoprmlnprm  16812  cshwshashlem1  17180  psgnunilem4  19598  lmodvsdi  21043  xrsdsreclblem  21600  nzerooringczr  21667  cpmatacl  22910  riinopn  23102  0ntr  23265  elcls  23267  hausnei2  23547  fgfil  24069  alexsubALTlem2  24242  alexsubALT  24245  aalioulem3  26534  aalioulem4  26535  wilthlem3  27271  2sqreultlem  27648  2sqreunnltlem  27651  bdayfinbndlem1  28697  finsumvtxdg2size  29937  upgrewlkle2  29993  upgrwlkdvdelem  30122  uhgrwkspthlem2  30140  clwwlkinwwlk  30428  wwlksext2clwwlk  30445  1pthon2v  30541  n4cyclfrgr  30679  frgrnbnb  30681  frgrwopreglem4a  30698  frgrreg  30782  frgrregord013  30783  grpoidinvlem3  30895  elspansn5  31963  atcv1  32769  atcvatlem  32774  chirredlem3  32781  mdsymlem3  32794  mdsymlem5  32796  mdsymlem6  32797  sumdmdlem2  32808  f1o3d  33008  slmdvsdi  33566  satfv0fun  35884  satffunlem1lem1  35915  satffunlem2lem1  35917  fgmin  36922  nndivsub  37009  mblfinlem3  38351  rngonegrmul  38636  crngm23  38694  hlrelat2  40218  pmaple  40576  pmodlem2  40662  dalaw  40701  sn-sup2  43306  syl5imp  45262  com3rgbi  45264  ee223  45384  relpmin  45702  2tceilhalfelfzo1  48114  iccpartigtl  48213  iccelpart  48223  lighneallem3  48400  bgoldbtbndlem3  48613  uhgrimisgrgric  48737  clnbgrgrim  48740  clnbgr3stgrgrlic  48826  gpgusgralem  48862  gpgvtxedg0  48869  gpgvtxedg1  48870  ply1mulgsumlem1  49207  fllog2  49389