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  625  impidc  860  pm2.61dc  867  3com23  1212  expcomd  1462  spimth  1759  sbiedh  1811  eqrdav  2205  necon4bbiddc  2451  ralrimdva  2587  ralrimdvva  2592  ceqsalt  2800  vtoclgft  2825  reu6  2964  sbciegft  3031  reuss2  3455  reupick  3459  reusv3  4512  ssrel  4768  ssrel2  4770  ssrelrel  4780  ssrelrn  4875  funssres  5319  funcnvuni  5349  fv3  5609  fvmptt  5681  funfvima2  5827  isoini  5897  isopolem  5901  f1ocnv2d  6160  f1o2ndf1  6324  nnmordi  6612  nnmord  6613  xpdom2  6938  findcard2  6998  findcard2s  6999  findcard2d  7000  findcard2sd  7001  xpfi  7041  ordiso2  7149  updjud  7196  genpcdl  7645  genpcuu  7646  distrlem5prl  7712  distrlem5pru  7713  lemul12a  8948  divgt0  8958  divge0  8959  lbreu  9031  bndndx  9307  elnnz  9395  nzadd  9438  fzind  9501  fnn0ind  9502  eqreznegel  9748  lbzbi  9750  irradd  9780  irrmul  9781  ledivge1le  9861  iccid  10060  uzsubsubfz  10182  fzrevral  10240  elfz0fzfz0  10261  fz0fzelfz0  10262  elfzmlbp  10267  elincfzoext  10335  elfzodifsumelfzo  10343  ssfzo12bi  10367  elfzonelfzo  10372  flqeqceilz  10476  le2sq2  10773  facdiv  10896  facwordi  10898  faclbnd  10899  fundm2domnop0  11003  swrdswrdlem  11169  swrdswrd  11170  cau3lem  11475  mulcn2  11673  climcau  11708  climcaucn  11712  modfsummod  11819  p1modz1  12155  dvdsdivcl  12211  ltoddhalfle  12254  halfleoddlt  12255  ndvdssub  12291  dfgcd2  12385  coprmdvds1  12463  coprmdvds  12464  coprmdvds2  12465  divgcdcoprm0  12473  cncongr1  12475  cncongr2  12476  prmfac1  12524  pcqcl  12679  dvdsprmpweqle  12710  oddprmdvds  12727  prmpwdvds  12728  infpnlem1  12732  lidrididd  13264  mulgaddcom  13532  mulginvcom  13533  imasabl  13722  lmodfopnelem1  14136  lss1d  14195  rnglidlmcl  14292  znrrg  14472  uniopn  14523  tgcnp  14731  iscnp4  14740  lmtopcnp  14772  txlm  14801  metss  15016  metcnp3  15033  logbgcd1irr  15489  gausslemma2dlem1a  15585  gausslemma2dlem2  15589  gausslemma2dlem3  15590  lgsquad2lem2  15609  2lgslem1a1  15613  2sqlem6  15647  bj-rspgt  15836