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  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  4604  ssrel  4861  ssrel2  4863  ssrelrel  4873  ssrelrn  4970  funssres  5418  funcnvuni  5448  f1ssf1  5669  fv3  5716  fvmptt  5794  funfvima2  5945  isoini  6018  isopolem  6022  f1ocnv2d  6288  f1o3d  6292  f1o2ndf1  6458  suppfnss  6491  suppssdc  6494  nnmordi  6783  nnmord  6784  xpdom2  7123  findcard2  7187  findcard2s  7188  findcard2d  7189  findcard2sd  7190  xpfi  7233  ordiso2  7369  updjud  7416  genpcdl  7880  genpcuu  7881  distrlem5prl  7947  distrlem5pru  7948  lemul12a  9186  divgt0  9196  divge0  9197  lbreu  9269  bndndx  9545  elnnz  9637  nzadd  9680  fzind  9744  fnn0ind  9745  eqreznegel  9997  lbzbi  9999  irradd  10029  irrmul  10030  ledivge1le  10110  iccid  10310  uzsubsubfz  10435  fzrevral  10495  elfz0fzfz0  10516  fz0fzelfz0  10517  elfzmlbp  10522  elincfzoext  10594  elfzodifsumelfzo  10602  ssfzo12bi  10626  elfzonelfzo  10631  flqeqceilz  10738  le2sq2  11035  facdiv  11159  facwordi  11161  faclbnd  11162  fundm2domnop0  11283  swrdswrdlem  11459  swrdswrd  11460  ccatopth2  11472  wrd2ind  11478  pfxccatin12lem2a  11482  swrdccatin2  11484  pfxccatin12lem2  11486  pfxccatin12lem3  11487  swrdccat  11490  swrdccat3blem  11494  reuccatpfxs1lem  11501  cau3lem  11863  mulcn2  12061  climcau  12096  climcaucn  12100  modfsummod  12208  p1modz1  12544  dvdsdivcl  12600  ltoddhalfle  12643  halfleoddlt  12644  ndvdssub  12680  dfgcd2  12774  coprmdvds1  12852  coprmdvds  12853  coprmdvds2  12854  divgcdcoprm0  12862  cncongr1  12864  cncongr2  12865  prmfac1  12913  pcqcl  13068  dvdsprmpweqle  13099  oddprmdvds  13116  prmpwdvds  13117  infpnlem1  13121  lidrididd  13685  mulgaddcom  13932  mulginvcom  13933  imasabl  14123  gsumvalfi  14135  lmodfopnelem1  14644  lss1d  14703  rnglidlmcl  14800  znrrg  14978  uniopn  15085  tgcnp  15293  iscnp4  15302  lmtopcnp  15334  txlm  15363  metss  15578  metcnp3  15595  logbgcd1irr  16052  gausslemma2dlem1a  16160  gausslemma2dlem2  16164  gausslemma2dlem3  16165  lgsquad2lem2  16184  2lgslem1a1  16188  2sqlem6  16222  umgrnloop  16340  upgredgpr  16373  usgrausgrben  16396  usgredg2vlem2  16447  ushgredgedg  16450  ushgredgedgloop  16452  wlk1walkdom  16583  uspgr2wlkeqi  16591  clwwlk1loop  16623  clwwlkccatlem  16624  umgrclwwlkge2  16626  clwwlknonex2lem2  16662  clwwlknonex2  16663  lealltlt2  16735  bj-rspgt  16797