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  865  pm2.61dc  872  3com23  1235  expcomd  1486  spimth  1783  sbiedh  1835  eqrdav  2230  necon4bbiddc  2476  ralrimdva  2612  ralrimdvva  2617  ceqsalt  2829  vtoclgft  2854  reu6  2995  sbciegft  3062  reuss2  3487  reupick  3491  reusv3  4557  ssrel  4814  ssrel2  4816  ssrelrel  4826  ssrelrn  4922  funssres  5369  funcnvuni  5399  f1ssf1  5615  fv3  5662  fvmptt  5738  funfvima2  5887  isoini  5959  isopolem  5963  f1ocnv2d  6227  f1o2ndf1  6393  nnmordi  6684  nnmord  6685  xpdom2  7015  findcard2  7078  findcard2s  7079  findcard2d  7080  findcard2sd  7081  xpfi  7124  ordiso2  7234  updjud  7281  genpcdl  7739  genpcuu  7740  distrlem5prl  7806  distrlem5pru  7807  lemul12a  9042  divgt0  9052  divge0  9053  lbreu  9125  bndndx  9401  elnnz  9489  nzadd  9532  fzind  9595  fnn0ind  9596  eqreznegel  9848  lbzbi  9850  irradd  9880  irrmul  9881  ledivge1le  9961  iccid  10160  uzsubsubfz  10282  fzrevral  10340  elfz0fzfz0  10361  fz0fzelfz0  10362  elfzmlbp  10367  elincfzoext  10439  elfzodifsumelfzo  10447  ssfzo12bi  10471  elfzonelfzo  10476  flqeqceilz  10581  le2sq2  10878  facdiv  11001  facwordi  11003  faclbnd  11004  fundm2domnop0  11113  swrdswrdlem  11289  swrdswrd  11290  ccatopth2  11302  wrd2ind  11308  pfxccatin12lem2a  11312  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  swrdccat  11320  swrdccat3blem  11324  reuccatpfxs1lem  11331  cau3lem  11679  mulcn2  11877  climcau  11912  climcaucn  11916  modfsummod  12024  p1modz1  12360  dvdsdivcl  12416  ltoddhalfle  12459  halfleoddlt  12460  ndvdssub  12496  dfgcd2  12590  coprmdvds1  12668  coprmdvds  12669  coprmdvds2  12670  divgcdcoprm0  12678  cncongr1  12680  cncongr2  12681  prmfac1  12729  pcqcl  12884  dvdsprmpweqle  12915  oddprmdvds  12932  prmpwdvds  12933  infpnlem1  12937  lidrididd  13470  mulgaddcom  13738  mulginvcom  13739  imasabl  13928  lmodfopnelem1  14344  lss1d  14403  rnglidlmcl  14500  znrrg  14680  uniopn  14731  tgcnp  14939  iscnp4  14948  lmtopcnp  14980  txlm  15009  metss  15224  metcnp3  15241  logbgcd1irr  15697  gausslemma2dlem1a  15793  gausslemma2dlem2  15797  gausslemma2dlem3  15798  lgsquad2lem2  15817  2lgslem1a1  15821  2sqlem6  15855  umgrnloop  15973  upgredgpr  16006  usgrausgrben  16029  usgredg2vlem2  16080  ushgredgedg  16083  ushgredgedgloop  16085  wlk1walkdom  16216  uspgr2wlkeqi  16224  clwwlk1loop  16256  clwwlkccatlem  16257  umgrclwwlkge2  16259  clwwlknonex2lem2  16295  clwwlknonex2  16296  bj-rspgt  16408  gfsumval  16706