Theorem com23 78

Description: Commutation of antecedents. Swap 2nd and 3rd. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis

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

Assertion

Ref	Expression
com23	⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Proof of Theorem com23

Step	Hyp	Ref	Expression
1		com3.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2		pm2.27 40	. 2 ⊢ (𝜒 → ((𝜒 → 𝜃) → 𝜃))
3	1, 2	syl9 72	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:  com3r  79  com13  80  pm2.04  82  pm2.86d  100  impcomd  255  impancom  260  a2and  564  con2d  633  impidc  870  pm2.61dc  877  3com23  1240  expcomd  1491  spimth  1788  sbiedh  1840  eqrdav  2237  necon4bbiddc  2494  ralrimdva  2630  ralrimdvva  2635  ceqsalt  2848  vtoclgft  2873  reu6  3015  sbciegft  3082  reuss2  3513  reupick  3517  reusv3  4608  ssrel  4865  ssrel2  4867  ssrelrel  4877  ssrelrn  4974  funssres  5423  funcnvuni  5453  f1ssf1  5674  fv3  5721  fvmptt  5800  funfvima2  5954  isoini  6027  isopolem  6031  f1ocnv2d  6297  f1o3d  6301  f1o2ndf1  6468  suppfnss  6501  suppssdc  6504  nnmordi  6794  nnmord  6795  xpdom2  7135  findcard2  7199  findcard2s  7200  findcard2d  7201  findcard2sd  7202  xpfi  7245  ordiso2  7382  updjud  7429  genpcdl  7893  genpcuu  7894  distrlem5prl  7960  distrlem5pru  7961  lemul12a  9201  divgt0  9211  divge0  9212  lbreu  9284  bndndx  9574  elnnz  9664  nzadd  9707  fzind  9772  fnn0ind  9773  eqreznegel  10030  lbzbi  10032  irradd  10062  irrmul  10064  ledivge1le  10144  iccid  10344  uzsubsubfz  10469  fzrevral  10529  elfz0fzfz0  10550  fz0fzelfz0  10551  elfzmlbp  10556  elincfzoext  10628  elfzodifsumelfzo  10636  ssfzo12bi  10660  elfzonelfzo  10665  flqeqceilz  10776  le2sq2  11073  facdiv  11198  facwordi  11200  faclbnd  11201  fundm2domnop0  11322  swrdswrdlem  11498  swrdswrd  11499  ccatopth2  11511  wrd2ind  11517  pfxccatin12lem2a  11521  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12lem3  11526  swrdccat  11529  swrdccat3blem  11533  reuccatpfxs1lem  11540  cau3lem  11903  mulcn2  12103  climcau  12138  climcaucn  12142  modfsummod  12250  p1modz1  12586  dvdsdivcl  12642  ltoddhalfle  12685  halfleoddlt  12686  ndvdssub  12722  dfgcd2  12816  coprmdvds1  12894  coprmdvds  12895  coprmdvds2  12896  divgcdcoprm0  12904  cncongr1  12906  cncongr2  12907  prmfac1  12956  pcqcl  13114  dvdsprmpweqle  13145  oddprmdvds  13162  prmpwdvds  13163  infpnlem1  13167  lidrididd  13761  mulgaddcom  14008  mulginvcom  14009  imasabl  14230  gsumvalfi  14242  lmodfopnelem1  14770  lss1d  14829  rnglidlmcl  14926  znrrg  15104  uniopn  15260  tgcnp  15468  iscnp4  15477  lmtopcnp  15509  txlm  15538  metss  15753  metcnp3  15770  logbgcd1irr  16236  gausslemma2dlem1a  16415  gausslemma2dlem2  16419  gausslemma2dlem3  16420  lgsquad2lem2  16439  2lgslem1a1  16443  2sqlem6  16477  umgrnloop  16595  upgredgpr  16628  usgrausgrben  16651  usgredg2vlem2  16702  ushgredgedg  16705  ushgredgedgloop  16707  wlk1walkdom  16838  uspgr2wlkeqi  16846  clwwlk1loop  16878  clwwlkccatlem  16879  umgrclwwlkge2  16881  clwwlknonex2lem2  16917  clwwlknonex2  16918  lealltlt2  16990  bj-rspgt  17052