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  1746  sbiedh  1798  eqrdav  2192  necon4bbiddc  2438  ralrimdva  2574  ralrimdvva  2579  ceqsalt  2786  vtoclgft  2810  reu6  2949  sbciegft  3016  reuss2  3439  reupick  3443  reusv3  4491  ssrel  4747  ssrel2  4749  ssrelrel  4759  funssres  5296  funcnvuni  5323  fv3  5577  fvmptt  5649  funfvima2  5791  isoini  5861  isopolem  5865  f1ocnv2d  6122  f1o2ndf1  6281  nnmordi  6569  nnmord  6570  xpdom2  6885  findcard2  6945  findcard2s  6946  findcard2d  6947  findcard2sd  6948  xpfi  6986  ordiso2  7094  updjud  7141  genpcdl  7579  genpcuu  7580  distrlem5prl  7646  distrlem5pru  7647  lemul12a  8881  divgt0  8891  divge0  8892  lbreu  8964  bndndx  9239  elnnz  9327  nzadd  9369  fzind  9432  fnn0ind  9433  eqreznegel  9679  lbzbi  9681  irradd  9711  irrmul  9712  ledivge1le  9792  iccid  9991  uzsubsubfz  10113  fzrevral  10171  elfz0fzfz0  10192  fz0fzelfz0  10193  elfzmlbp  10198  elfzodifsumelfzo  10268  ssfzo12bi  10292  elfzonelfzo  10297  flqeqceilz  10389  le2sq2  10686  facdiv  10809  facwordi  10811  faclbnd  10812  cau3lem  11258  mulcn2  11455  climcau  11490  climcaucn  11494  modfsummod  11601  p1modz1  11937  dvdsdivcl  11992  ltoddhalfle  12034  halfleoddlt  12035  ndvdssub  12071  dfgcd2  12151  coprmdvds1  12229  coprmdvds  12230  coprmdvds2  12231  divgcdcoprm0  12239  cncongr1  12241  cncongr2  12242  prmfac1  12290  pcqcl  12444  dvdsprmpweqle  12475  oddprmdvds  12492  prmpwdvds  12493  infpnlem1  12497  lidrididd  12965  mulgaddcom  13216  mulginvcom  13217  imasabl  13406  lmodfopnelem1  13820  lss1d  13879  rnglidlmcl  13976  znrrg  14148  uniopn  14169  tgcnp  14377  iscnp4  14386  lmtopcnp  14418  txlm  14447  metss  14662  metcnp3  14679  logbgcd1irr  15099  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  gausslemma2dlem3  15179  2sqlem6  15207  bj-rspgt  15278