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 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

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  93  com35  99  3an1rs  1378  rspct  3568  po2nr  5585  wefrc  5657  tz7.7  6388  funssres  6582  isomin  7337  f1ocnv2d  7665  onint  7790  f1oweALT  7970  bropfvvvv  8088  tfrlem9  8373  tz7.49  8433  oelim  8520  oaordex  8544  omordi  8552  omass  8566  oen0  8573  nnmass  8611  nnmordi  8618  inf3lem2  9599  epfrs  9701  indcardi  10026  ackbij1lem16  10218  cfcoflem  10257  axcc3  10423  zorn2lem7  10487  grur1a  10805  genpcd  10992  genpnmax  10993  mulclprlem  11005  distrlem1pr  11011  ltaddpr  11020  ltexprlem6  11027  ltexprlem7  11028  mulgt0sr  11091  divgt0  12084  divge0  12085  sup2  12172  uzind2  12690  uzwo  12936  supxrun  13343  expnbnd  14270  facdiv  14325  hashimarni  14480  swrdswrdlem  14743  wrd2ind  14762  s3iunsndisj  15007  caubnd  15412  dvdsabseq  16372  lcmfunsnlem2lem1  16697  divgcdcoprm0  16724  ncoprmlnprm  16788  cshwshashlem1  17156  psgnunilem4  19568  lmodvsdi  20987  xrsdsreclblem  21544  nzerooringczr  21611  cpmatacl  22854  riinopn  23046  0ntr  23209  elcls  23211  hausnei2  23491  fgfil  24013  alexsubALTlem2  24186  alexsubALT  24189  aalioulem3  26478  aalioulem4  26479  wilthlem3  27215  2sqreultlem  27592  2sqreunnltlem  27595  bdayfinbndlem1  28641  finsumvtxdg2size  29881  upgrewlkle2  29937  upgrwlkdvdelem  30066  uhgrwkspthlem2  30084  clwwlkinwwlk  30372  wwlksext2clwwlk  30389  1pthon2v  30485  n4cyclfrgr  30623  frgrnbnb  30625  frgrwopreglem4a  30642  frgrreg  30726  frgrregord013  30727  grpoidinvlem3  30839  elspansn5  31907  atcv1  32713  atcvatlem  32718  chirredlem3  32725  mdsymlem3  32738  mdsymlem5  32740  mdsymlem6  32741  sumdmdlem2  32752  f1o3d  32952  slmdvsdi  33516  satfv0fun  35844  satffunlem1lem1  35875  satffunlem2lem1  35877  fgmin  36862  nndivsub  36949  mblfinlem3  38291  rngonegrmul  38576  crngm23  38634  hlrelat2  40158  pmaple  40516  pmodlem2  40602  dalaw  40641  sn-sup2  43246  syl5imp  45204  com3rgbi  45206  ee223  45326  relpmin  45644  2tceilhalfelfzo1  48056  iccpartigtl  48155  iccelpart  48165  lighneallem3  48342  bgoldbtbndlem3  48555  uhgrimisgrgric  48679  clnbgrgrim  48682  clnbgr3stgrgrlic  48768  gpgusgralem  48804  gpgvtxedg0  48811  gpgvtxedg1  48812  ply1mulgsumlem1  49149  fllog2  49331