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  1784  sbiedh  1836  eqrdav  2231  necon4bbiddc  2486  ralrimdva  2622  ralrimdvva  2627  ceqsalt  2839  vtoclgft  2864  reu6  3005  sbciegft  3072  reuss2  3500  reupick  3504  reusv3  4580  ssrel  4837  ssrel2  4839  ssrelrel  4849  ssrelrn  4946  funssres  5394  funcnvuni  5424  f1ssf1  5645  fv3  5692  fvmptt  5768  funfvima2  5918  isoini  5990  isopolem  5994  f1ocnv2d  6258  f1o2ndf1  6423  suppfnss  6456  suppssdc  6459  nnmordi  6748  nnmord  6749  xpdom2  7081  findcard2  7145  findcard2s  7146  findcard2d  7147  findcard2sd  7148  xpfi  7191  ordiso2  7325  updjud  7372  genpcdl  7833  genpcuu  7834  distrlem5prl  7900  distrlem5pru  7901  lemul12a  9135  divgt0  9145  divge0  9146  lbreu  9218  bndndx  9494  elnnz  9586  nzadd  9629  fzind  9692  fnn0ind  9693  eqreznegel  9945  lbzbi  9947  irradd  9977  irrmul  9978  ledivge1le  10058  iccid  10257  uzsubsubfz  10380  fzrevral  10438  elfz0fzfz0  10459  fz0fzelfz0  10460  elfzmlbp  10465  elincfzoext  10537  elfzodifsumelfzo  10545  ssfzo12bi  10569  elfzonelfzo  10574  flqeqceilz  10679  le2sq2  10976  facdiv  11099  facwordi  11101  faclbnd  11102  fundm2domnop0  11216  swrdswrdlem  11392  swrdswrd  11393  ccatopth2  11405  wrd2ind  11411  pfxccatin12lem2a  11415  swrdccatin2  11417  pfxccatin12lem2  11419  pfxccatin12lem3  11420  swrdccat  11423  swrdccat3blem  11427  reuccatpfxs1lem  11434  cau3lem  11795  mulcn2  11993  climcau  12028  climcaucn  12032  modfsummod  12140  p1modz1  12476  dvdsdivcl  12532  ltoddhalfle  12575  halfleoddlt  12576  ndvdssub  12612  dfgcd2  12706  coprmdvds1  12784  coprmdvds  12785  coprmdvds2  12786  divgcdcoprm0  12794  cncongr1  12796  cncongr2  12797  prmfac1  12845  pcqcl  13000  dvdsprmpweqle  13031  oddprmdvds  13048  prmpwdvds  13049  infpnlem1  13053  lidrididd  13587  mulgaddcom  13855  mulginvcom  13856  imasabl  14045  lmodfopnelem1  14464  lss1d  14523  rnglidlmcl  14620  znrrg  14800  uniopn  14858  tgcnp  15066  iscnp4  15075  lmtopcnp  15107  txlm  15136  metss  15351  metcnp3  15368  logbgcd1irr  15824  gausslemma2dlem1a  15923  gausslemma2dlem2  15927  gausslemma2dlem3  15928  lgsquad2lem2  15947  2lgslem1a1  15951  2sqlem6  15985  umgrnloop  16103  upgredgpr  16136  usgrausgrben  16159  usgredg2vlem2  16210  ushgredgedg  16213  ushgredgedgloop  16215  wlk1walkdom  16346  uspgr2wlkeqi  16354  clwwlk1loop  16386  clwwlkccatlem  16387  umgrclwwlkge2  16389  clwwlknonex2lem2  16425  clwwlknonex2  16426  bj-rspgt  16550  gfsumval  16853