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  624  impidc  858  pm2.61dc  865  3com23  1209  expcomd  1441  spimth  1735  sbiedh  1787  eqrdav  2176  necon4bbiddc  2421  ralrimdva  2557  ralrimdvva  2562  ceqsalt  2765  vtoclgft  2789  reu6  2928  sbciegft  2995  reuss2  3417  reupick  3421  reusv3  4462  ssrel  4716  ssrel2  4718  ssrelrel  4728  funssres  5260  funcnvuni  5287  fv3  5540  fvmptt  5609  funfvima2  5751  isoini  5821  isopolem  5825  f1ocnv2d  6077  f1o2ndf1  6231  nnmordi  6519  nnmord  6520  xpdom2  6833  findcard2  6891  findcard2s  6892  findcard2d  6893  findcard2sd  6894  xpfi  6931  ordiso2  7036  updjud  7083  genpcdl  7520  genpcuu  7521  distrlem5prl  7587  distrlem5pru  7588  lemul12a  8821  divgt0  8831  divge0  8832  lbreu  8904  bndndx  9177  elnnz  9265  nzadd  9307  fzind  9370  fnn0ind  9371  eqreznegel  9616  lbzbi  9618  irradd  9648  irrmul  9649  ledivge1le  9728  iccid  9927  uzsubsubfz  10049  fzrevral  10107  elfz0fzfz0  10128  fz0fzelfz0  10129  elfzmlbp  10134  elfzodifsumelfzo  10203  ssfzo12bi  10227  elfzonelfzo  10232  flqeqceilz  10320  le2sq2  10598  facdiv  10720  facwordi  10722  faclbnd  10723  cau3lem  11125  mulcn2  11322  climcau  11357  climcaucn  11361  modfsummod  11468  p1modz1  11803  dvdsdivcl  11858  ltoddhalfle  11900  halfleoddlt  11901  ndvdssub  11937  dfgcd2  12017  coprmdvds1  12093  coprmdvds  12094  coprmdvds2  12095  divgcdcoprm0  12103  cncongr1  12105  cncongr2  12106  prmfac1  12154  pcqcl  12308  dvdsprmpweqle  12338  oddprmdvds  12354  prmpwdvds  12355  infpnlem1  12359  lidrididd  12806  mulgaddcom  13012  mulginvcom  13013  lmodfopnelem1  13419  lss1d  13475  uniopn  13586  tgcnp  13794  iscnp4  13803  lmtopcnp  13835  txlm  13864  metss  14079  metcnp3  14096  logbgcd1irr  14470  2sqlem6  14552  bj-rspgt  14623