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  859  pm2.61dc  866  3com23  1211  expcomd  1452  spimth  1749  sbiedh  1801  eqrdav  2195  necon4bbiddc  2441  ralrimdva  2577  ralrimdvva  2582  ceqsalt  2789  vtoclgft  2814  reu6  2953  sbciegft  3020  reuss2  3444  reupick  3448  reusv3  4496  ssrel  4752  ssrel2  4754  ssrelrel  4764  funssres  5301  funcnvuni  5328  fv3  5584  fvmptt  5656  funfvima2  5798  isoini  5868  isopolem  5872  f1ocnv2d  6131  f1o2ndf1  6295  nnmordi  6583  nnmord  6584  xpdom2  6899  findcard2  6959  findcard2s  6960  findcard2d  6961  findcard2sd  6962  xpfi  7002  ordiso2  7110  updjud  7157  genpcdl  7603  genpcuu  7604  distrlem5prl  7670  distrlem5pru  7671  lemul12a  8906  divgt0  8916  divge0  8917  lbreu  8989  bndndx  9265  elnnz  9353  nzadd  9395  fzind  9458  fnn0ind  9459  eqreznegel  9705  lbzbi  9707  irradd  9737  irrmul  9738  ledivge1le  9818  iccid  10017  uzsubsubfz  10139  fzrevral  10197  elfz0fzfz0  10218  fz0fzelfz0  10219  elfzmlbp  10224  elfzodifsumelfzo  10294  ssfzo12bi  10318  elfzonelfzo  10323  flqeqceilz  10427  le2sq2  10724  facdiv  10847  facwordi  10849  faclbnd  10850  cau3lem  11296  mulcn2  11494  climcau  11529  climcaucn  11533  modfsummod  11640  p1modz1  11976  dvdsdivcl  12032  ltoddhalfle  12075  halfleoddlt  12076  ndvdssub  12112  dfgcd2  12206  coprmdvds1  12284  coprmdvds  12285  coprmdvds2  12286  divgcdcoprm0  12294  cncongr1  12296  cncongr2  12297  prmfac1  12345  pcqcl  12500  dvdsprmpweqle  12531  oddprmdvds  12548  prmpwdvds  12549  infpnlem1  12553  lidrididd  13084  mulgaddcom  13352  mulginvcom  13353  imasabl  13542  lmodfopnelem1  13956  lss1d  14015  rnglidlmcl  14112  znrrg  14292  uniopn  14321  tgcnp  14529  iscnp4  14538  lmtopcnp  14570  txlm  14599  metss  14814  metcnp3  14831  logbgcd1irr  15287  gausslemma2dlem1a  15383  gausslemma2dlem2  15387  gausslemma2dlem3  15388  lgsquad2lem2  15407  2lgslem1a1  15411  2sqlem6  15445  bj-rspgt  15516