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  4608  ssrel  4865  ssrel2  4867  ssrelrel  4877  ssrelrn  4974  funssres  5423  funcnvuni  5453  f1ssf1  5674  fv3  5721  fvmptt  5800  funfvima2  5954  isoini  6027  isopolem  6031  f1ocnv2d  6297  f1o3d  6301  f1o2ndf1  6468  suppfnss  6501  suppssdc  6504  nnmordi  6793  nnmord  6794  xpdom2  7134  findcard2  7198  findcard2s  7199  findcard2d  7200  findcard2sd  7201  xpfi  7244  ordiso2  7382  updjud  7429  genpcdl  7893  genpcuu  7894  distrlem5prl  7960  distrlem5pru  7961  lemul12a  9201  divgt0  9211  divge0  9212  lbreu  9284  bndndx  9574  elnnz  9666  nzadd  9709  fzind  9773  fnn0ind  9774  eqreznegel  10031  lbzbi  10033  irradd  10063  irrmul  10065  ledivge1le  10145  iccid  10345  uzsubsubfz  10470  fzrevral  10530  elfz0fzfz0  10551  fz0fzelfz0  10552  elfzmlbp  10557  elincfzoext  10629  elfzodifsumelfzo  10637  ssfzo12bi  10661  elfzonelfzo  10666  flqeqceilz  10777  le2sq2  11074  facdiv  11199  facwordi  11201  faclbnd  11202  fundm2domnop0  11323  swrdswrdlem  11499  swrdswrd  11500  ccatopth2  11512  wrd2ind  11518  pfxccatin12lem2a  11522  swrdccatin2  11524  pfxccatin12lem2  11526  pfxccatin12lem3  11527  swrdccat  11530  swrdccat3blem  11534  reuccatpfxs1lem  11541  cau3lem  11904  mulcn2  12104  climcau  12139  climcaucn  12143  modfsummod  12251  p1modz1  12587  dvdsdivcl  12643  ltoddhalfle  12686  halfleoddlt  12687  ndvdssub  12723  dfgcd2  12817  coprmdvds1  12895  coprmdvds  12896  coprmdvds2  12897  divgcdcoprm0  12905  cncongr1  12907  cncongr2  12908  prmfac1  12957  pcqcl  13115  dvdsprmpweqle  13146  oddprmdvds  13163  prmpwdvds  13164  infpnlem1  13168  lidrididd  13762  mulgaddcom  14009  mulginvcom  14010  imasabl  14231  gsumvalfi  14243  lmodfopnelem1  14771  lss1d  14830  rnglidlmcl  14927  znrrg  15105  uniopn  15239  tgcnp  15447  iscnp4  15456  lmtopcnp  15488  txlm  15517  metss  15732  metcnp3  15749  logbgcd1irr  16215  gausslemma2dlem1a  16394  gausslemma2dlem2  16398  gausslemma2dlem3  16399  lgsquad2lem2  16418  2lgslem1a1  16422  2sqlem6  16456  umgrnloop  16574  upgredgpr  16607  usgrausgrben  16630  usgredg2vlem2  16681  ushgredgedg  16684  ushgredgedgloop  16686  wlk1walkdom  16817  uspgr2wlkeqi  16825  clwwlk1loop  16857  clwwlkccatlem  16858  umgrclwwlkge2  16860  clwwlknonex2lem2  16896  clwwlknonex2  16897  lealltlt2  16969  bj-rspgt  17031