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  627  impidc  863  pm2.61dc  870  3com23  1233  expcomd  1484  spimth  1781  sbiedh  1833  eqrdav  2228  necon4bbiddc  2474  ralrimdva  2610  ralrimdvva  2615  ceqsalt  2826  vtoclgft  2851  reu6  2992  sbciegft  3059  reuss2  3484  reupick  3488  reusv3  4548  ssrel  4804  ssrel2  4806  ssrelrel  4816  ssrelrn  4911  funssres  5356  funcnvuni  5386  fv3  5646  fvmptt  5719  funfvima2  5865  isoini  5935  isopolem  5939  f1ocnv2d  6200  f1o2ndf1  6364  nnmordi  6652  nnmord  6653  xpdom2  6978  findcard2  7039  findcard2s  7040  findcard2d  7041  findcard2sd  7042  xpfi  7082  ordiso2  7190  updjud  7237  genpcdl  7694  genpcuu  7695  distrlem5prl  7761  distrlem5pru  7762  lemul12a  8997  divgt0  9007  divge0  9008  lbreu  9080  bndndx  9356  elnnz  9444  nzadd  9487  fzind  9550  fnn0ind  9551  eqreznegel  9797  lbzbi  9799  irradd  9829  irrmul  9830  ledivge1le  9910  iccid  10109  uzsubsubfz  10231  fzrevral  10289  elfz0fzfz0  10310  fz0fzelfz0  10311  elfzmlbp  10316  elincfzoext  10386  elfzodifsumelfzo  10394  ssfzo12bi  10418  elfzonelfzo  10423  flqeqceilz  10527  le2sq2  10824  facdiv  10947  facwordi  10949  faclbnd  10950  fundm2domnop0  11054  swrdswrdlem  11222  swrdswrd  11223  ccatopth2  11235  wrd2ind  11241  pfxccatin12lem2a  11245  swrdccatin2  11247  pfxccatin12lem2  11249  pfxccatin12lem3  11250  swrdccat  11253  swrdccat3blem  11257  reuccatpfxs1lem  11264  cau3lem  11611  mulcn2  11809  climcau  11844  climcaucn  11848  modfsummod  11955  p1modz1  12291  dvdsdivcl  12347  ltoddhalfle  12390  halfleoddlt  12391  ndvdssub  12427  dfgcd2  12521  coprmdvds1  12599  coprmdvds  12600  coprmdvds2  12601  divgcdcoprm0  12609  cncongr1  12611  cncongr2  12612  prmfac1  12660  pcqcl  12815  dvdsprmpweqle  12846  oddprmdvds  12863  prmpwdvds  12864  infpnlem1  12868  lidrididd  13401  mulgaddcom  13669  mulginvcom  13670  imasabl  13859  lmodfopnelem1  14273  lss1d  14332  rnglidlmcl  14429  znrrg  14609  uniopn  14660  tgcnp  14868  iscnp4  14877  lmtopcnp  14909  txlm  14938  metss  15153  metcnp3  15170  logbgcd1irr  15626  gausslemma2dlem1a  15722  gausslemma2dlem2  15726  gausslemma2dlem3  15727  lgsquad2lem2  15746  2lgslem1a1  15750  2sqlem6  15784  umgrnloop  15901  upgredgpr  15932  usgrausgrben  15955  usgredg2vlem2  16006  ushgredgedg  16009  ushgredgedgloop  16011  bj-rspgt  16080