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

Syntax hints:   → wi 4

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

This theorem is referenced by:  com3r  79  com13  80  pm2.04  82  pm2.86d  100  impcomd  255  impancom  260  a2and  560  con2d  629  impidc  866  pm2.61dc  873  3com23  1236  expcomd  1487  spimth  1783  sbiedh  1835  eqrdav  2230  necon4bbiddc  2477  ralrimdva  2613  ralrimdvva  2618  ceqsalt  2830  vtoclgft  2855  reu6  2996  sbciegft  3063  reuss2  3489  reupick  3493  reusv3  4563  ssrel  4820  ssrel2  4822  ssrelrel  4832  ssrelrn  4928  funssres  5376  funcnvuni  5406  f1ssf1  5624  fv3  5671  fvmptt  5747  funfvima2  5897  isoini  5969  isopolem  5973  f1ocnv2d  6237  f1o2ndf1  6402  suppfnss  6435  suppssdc  6438  nnmordi  6727  nnmord  6728  xpdom2  7058  findcard2  7121  findcard2s  7122  findcard2d  7123  findcard2sd  7124  xpfi  7167  ordiso2  7277  updjud  7324  genpcdl  7782  genpcuu  7783  distrlem5prl  7849  distrlem5pru  7850  lemul12a  9084  divgt0  9094  divge0  9095  lbreu  9167  bndndx  9443  elnnz  9533  nzadd  9576  fzind  9639  fnn0ind  9640  eqreznegel  9892  lbzbi  9894  irradd  9924  irrmul  9925  ledivge1le  10005  iccid  10204  uzsubsubfz  10327  fzrevral  10385  elfz0fzfz0  10406  fz0fzelfz0  10407  elfzmlbp  10412  elincfzoext  10484  elfzodifsumelfzo  10492  ssfzo12bi  10516  elfzonelfzo  10521  flqeqceilz  10626  le2sq2  10923  facdiv  11046  facwordi  11048  faclbnd  11049  fundm2domnop0  11158  swrdswrdlem  11334  swrdswrd  11335  ccatopth2  11347  wrd2ind  11353  pfxccatin12lem2a  11357  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12lem3  11362  swrdccat  11365  swrdccat3blem  11369  reuccatpfxs1lem  11376  cau3lem  11737  mulcn2  11935  climcau  11970  climcaucn  11974  modfsummod  12082  p1modz1  12418  dvdsdivcl  12474  ltoddhalfle  12517  halfleoddlt  12518  ndvdssub  12554  dfgcd2  12648  coprmdvds1  12726  coprmdvds  12727  coprmdvds2  12728  divgcdcoprm0  12736  cncongr1  12738  cncongr2  12739  prmfac1  12787  pcqcl  12942  dvdsprmpweqle  12973  oddprmdvds  12990  prmpwdvds  12991  infpnlem1  12995  lidrididd  13528  mulgaddcom  13796  mulginvcom  13797  imasabl  13986  lmodfopnelem1  14403  lss1d  14462  rnglidlmcl  14559  znrrg  14739  uniopn  14795  tgcnp  15003  iscnp4  15012  lmtopcnp  15044  txlm  15073  metss  15288  metcnp3  15305  logbgcd1irr  15761  gausslemma2dlem1a  15860  gausslemma2dlem2  15864  gausslemma2dlem3  15865  lgsquad2lem2  15884  2lgslem1a1  15888  2sqlem6  15922  umgrnloop  16040  upgredgpr  16073  usgrausgrben  16096  usgredg2vlem2  16147  ushgredgedg  16150  ushgredgedgloop  16152  wlk1walkdom  16283  uspgr2wlkeqi  16291  clwwlk1loop  16323  clwwlkccatlem  16324  umgrclwwlkge2  16326  clwwlknonex2lem2  16362  clwwlknonex2  16363  bj-rspgt  16487  gfsumval  16792