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  7376  updjud  7423  genpcdl  7887  genpcuu  7888  distrlem5prl  7954  distrlem5pru  7955  lemul12a  9195  divgt0  9205  divge0  9206  lbreu  9278  bndndx  9567  elnnz  9659  nzadd  9702  fzind  9766  fnn0ind  9767  eqreznegel  10024  lbzbi  10026  irradd  10056  irrmul  10058  ledivge1le  10138  iccid  10338  uzsubsubfz  10463  fzrevral  10523  elfz0fzfz0  10544  fz0fzelfz0  10545  elfzmlbp  10550  elincfzoext  10622  elfzodifsumelfzo  10630  ssfzo12bi  10654  elfzonelfzo  10659  flqeqceilz  10769  le2sq2  11066  facdiv  11191  facwordi  11193  faclbnd  11194  fundm2domnop0  11315  swrdswrdlem  11491  swrdswrd  11492  ccatopth2  11504  wrd2ind  11510  pfxccatin12lem2a  11514  swrdccatin2  11516  pfxccatin12lem2  11518  pfxccatin12lem3  11519  swrdccat  11522  swrdccat3blem  11526  reuccatpfxs1lem  11533  cau3lem  11896  mulcn2  12096  climcau  12131  climcaucn  12135  modfsummod  12243  p1modz1  12579  dvdsdivcl  12635  ltoddhalfle  12678  halfleoddlt  12679  ndvdssub  12715  dfgcd2  12809  coprmdvds1  12887  coprmdvds  12888  coprmdvds2  12889  divgcdcoprm0  12897  cncongr1  12899  cncongr2  12900  prmfac1  12949  pcqcl  13107  dvdsprmpweqle  13138  oddprmdvds  13155  prmpwdvds  13156  infpnlem1  13160  lidrididd  13753  mulgaddcom  14000  mulginvcom  14001  imasabl  14191  gsumvalfi  14203  lmodfopnelem1  14712  lss1d  14771  rnglidlmcl  14868  znrrg  15046  uniopn  15154  tgcnp  15362  iscnp4  15371  lmtopcnp  15403  txlm  15432  metss  15647  metcnp3  15664  logbgcd1irr  16125  gausslemma2dlem1a  16299  gausslemma2dlem2  16303  gausslemma2dlem3  16304  lgsquad2lem2  16323  2lgslem1a1  16327  2sqlem6  16361  umgrnloop  16479  upgredgpr  16512  usgrausgrben  16535  usgredg2vlem2  16586  ushgredgedg  16589  ushgredgedgloop  16591  wlk1walkdom  16722  uspgr2wlkeqi  16730  clwwlk1loop  16762  clwwlkccatlem  16763  umgrclwwlkge2  16765  clwwlknonex2lem2  16801  clwwlknonex2  16802  lealltlt2  16874  bj-rspgt  16936