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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  4606  ssrel  4863  ssrel2  4865  ssrelrel  4875  ssrelrn  4972  funssres  5420  funcnvuni  5450  f1ssf1  5671  fv3  5718  fvmptt  5797  funfvima2  5951  isoini  6024  isopolem  6028  f1ocnv2d  6294  f1o3d  6298  f1o2ndf1  6464  suppfnss  6497  suppssdc  6500  nnmordi  6789  nnmord  6790  xpdom2  7129  findcard2  7193  findcard2s  7194  findcard2d  7195  findcard2sd  7196  xpfi  7239  ordiso2  7375  updjud  7422  genpcdl  7886  genpcuu  7887  distrlem5prl  7953  distrlem5pru  7954  lemul12a  9193  divgt0  9203  divge0  9204  lbreu  9276  bndndx  9564  elnnz  9656  nzadd  9699  fzind  9763  fnn0ind  9764  eqreznegel  10016  lbzbi  10018  irradd  10048  irrmul  10049  ledivge1le  10129  iccid  10329  uzsubsubfz  10454  fzrevral  10514  elfz0fzfz0  10535  fz0fzelfz0  10536  elfzmlbp  10541  elincfzoext  10613  elfzodifsumelfzo  10621  ssfzo12bi  10645  elfzonelfzo  10650  flqeqceilz  10757  le2sq2  11054  facdiv  11178  facwordi  11180  faclbnd  11181  fundm2domnop0  11302  swrdswrdlem  11478  swrdswrd  11479  ccatopth2  11491  wrd2ind  11497  pfxccatin12lem2a  11501  swrdccatin2  11503  pfxccatin12lem2  11505  pfxccatin12lem3  11506  swrdccat  11509  swrdccat3blem  11513  reuccatpfxs1lem  11520  cau3lem  11882  mulcn2  12080  climcau  12115  climcaucn  12119  modfsummod  12227  p1modz1  12563  dvdsdivcl  12619  ltoddhalfle  12662  halfleoddlt  12663  ndvdssub  12699  dfgcd2  12793  coprmdvds1  12871  coprmdvds  12872  coprmdvds2  12873  divgcdcoprm0  12881  cncongr1  12883  cncongr2  12884  prmfac1  12932  pcqcl  13087  dvdsprmpweqle  13118  oddprmdvds  13135  prmpwdvds  13136  infpnlem1  13140  lidrididd  13704  mulgaddcom  13951  mulginvcom  13952  imasabl  14142  gsumvalfi  14154  lmodfopnelem1  14663  lss1d  14722  rnglidlmcl  14819  znrrg  14997  uniopn  15104  tgcnp  15312  iscnp4  15321  lmtopcnp  15353  txlm  15382  metss  15597  metcnp3  15614  logbgcd1irr  16075  gausslemma2dlem1a  16189  gausslemma2dlem2  16193  gausslemma2dlem3  16194  lgsquad2lem2  16213  2lgslem1a1  16217  2sqlem6  16251  umgrnloop  16369  upgredgpr  16402  usgrausgrben  16425  usgredg2vlem2  16476  ushgredgedg  16479  ushgredgedgloop  16481  wlk1walkdom  16612  uspgr2wlkeqi  16620  clwwlk1loop  16652  clwwlkccatlem  16653  umgrclwwlkge2  16655  clwwlknonex2lem2  16691  clwwlknonex2  16692  lealltlt2  16764  bj-rspgt  16826