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  558  con2d  627  impidc  863  pm2.61dc  870  3com23  1233  expcomd  1484  spimth  1781  sbiedh  1833  eqrdav  2228  necon4bbiddc  2474  ralrimdva  2610  ralrimdvva  2615  ceqsalt  2827  vtoclgft  2852  reu6  2993  sbciegft  3060  reuss2  3485  reupick  3489  reusv3  4555  ssrel  4812  ssrel2  4814  ssrelrel  4824  ssrelrn  4920  funssres  5366  funcnvuni  5396  fv3  5658  fvmptt  5734  funfvima2  5882  isoini  5954  isopolem  5958  f1ocnv2d  6222  f1o2ndf1  6388  nnmordi  6679  nnmord  6680  xpdom2  7010  findcard2  7073  findcard2s  7074  findcard2d  7075  findcard2sd  7076  xpfi  7119  ordiso2  7228  updjud  7275  genpcdl  7732  genpcuu  7733  distrlem5prl  7799  distrlem5pru  7800  lemul12a  9035  divgt0  9045  divge0  9046  lbreu  9118  bndndx  9394  elnnz  9482  nzadd  9525  fzind  9588  fnn0ind  9589  eqreznegel  9841  lbzbi  9843  irradd  9873  irrmul  9874  ledivge1le  9954  iccid  10153  uzsubsubfz  10275  fzrevral  10333  elfz0fzfz0  10354  fz0fzelfz0  10355  elfzmlbp  10360  elincfzoext  10431  elfzodifsumelfzo  10439  ssfzo12bi  10463  elfzonelfzo  10468  flqeqceilz  10573  le2sq2  10870  facdiv  10993  facwordi  10995  faclbnd  10996  fundm2domnop0  11102  swrdswrdlem  11278  swrdswrd  11279  ccatopth2  11291  wrd2ind  11297  pfxccatin12lem2a  11301  swrdccatin2  11303  pfxccatin12lem2  11305  pfxccatin12lem3  11306  swrdccat  11309  swrdccat3blem  11313  reuccatpfxs1lem  11320  cau3lem  11668  mulcn2  11866  climcau  11901  climcaucn  11905  modfsummod  12012  p1modz1  12348  dvdsdivcl  12404  ltoddhalfle  12447  halfleoddlt  12448  ndvdssub  12484  dfgcd2  12578  coprmdvds1  12656  coprmdvds  12657  coprmdvds2  12658  divgcdcoprm0  12666  cncongr1  12668  cncongr2  12669  prmfac1  12717  pcqcl  12872  dvdsprmpweqle  12903  oddprmdvds  12920  prmpwdvds  12921  infpnlem1  12925  lidrididd  13458  mulgaddcom  13726  mulginvcom  13727  imasabl  13916  lmodfopnelem1  14331  lss1d  14390  rnglidlmcl  14487  znrrg  14667  uniopn  14718  tgcnp  14926  iscnp4  14935  lmtopcnp  14967  txlm  14996  metss  15211  metcnp3  15228  logbgcd1irr  15684  gausslemma2dlem1a  15780  gausslemma2dlem2  15784  gausslemma2dlem3  15785  lgsquad2lem2  15804  2lgslem1a1  15808  2sqlem6  15842  umgrnloop  15960  upgredgpr  15993  usgrausgrben  16016  usgredg2vlem2  16067  ushgredgedg  16070  ushgredgedgloop  16072  wlk1walkdom  16170  uspgr2wlkeqi  16178  clwwlk1loop  16208  clwwlkccatlem  16209  umgrclwwlkge2  16211  clwwlknonex2lem2  16247  clwwlknonex2  16248  bj-rspgt  16332  gfsumval  16630