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  4552  ssrel  4809  ssrel2  4811  ssrelrel  4821  ssrelrn  4917  funssres  5363  funcnvuni  5393  fv3  5655  fvmptt  5731  funfvima2  5879  isoini  5951  isopolem  5955  f1ocnv2d  6219  f1o2ndf1  6385  nnmordi  6675  nnmord  6676  xpdom2  7003  findcard2  7064  findcard2s  7065  findcard2d  7066  findcard2sd  7067  xpfi  7110  ordiso2  7218  updjud  7265  genpcdl  7722  genpcuu  7723  distrlem5prl  7789  distrlem5pru  7790  lemul12a  9025  divgt0  9035  divge0  9036  lbreu  9108  bndndx  9384  elnnz  9472  nzadd  9515  fzind  9578  fnn0ind  9579  eqreznegel  9826  lbzbi  9828  irradd  9858  irrmul  9859  ledivge1le  9939  iccid  10138  uzsubsubfz  10260  fzrevral  10318  elfz0fzfz0  10339  fz0fzelfz0  10340  elfzmlbp  10345  elincfzoext  10416  elfzodifsumelfzo  10424  ssfzo12bi  10448  elfzonelfzo  10453  flqeqceilz  10557  le2sq2  10854  facdiv  10977  facwordi  10979  faclbnd  10980  fundm2domnop0  11085  swrdswrdlem  11257  swrdswrd  11258  ccatopth2  11270  wrd2ind  11276  pfxccatin12lem2a  11280  swrdccatin2  11282  pfxccatin12lem2  11284  pfxccatin12lem3  11285  swrdccat  11288  swrdccat3blem  11292  reuccatpfxs1lem  11299  cau3lem  11646  mulcn2  11844  climcau  11879  climcaucn  11883  modfsummod  11990  p1modz1  12326  dvdsdivcl  12382  ltoddhalfle  12425  halfleoddlt  12426  ndvdssub  12462  dfgcd2  12556  coprmdvds1  12634  coprmdvds  12635  coprmdvds2  12636  divgcdcoprm0  12644  cncongr1  12646  cncongr2  12647  prmfac1  12695  pcqcl  12850  dvdsprmpweqle  12881  oddprmdvds  12898  prmpwdvds  12899  infpnlem1  12903  lidrididd  13436  mulgaddcom  13704  mulginvcom  13705  imasabl  13894  lmodfopnelem1  14309  lss1d  14368  rnglidlmcl  14465  znrrg  14645  uniopn  14696  tgcnp  14904  iscnp4  14913  lmtopcnp  14945  txlm  14974  metss  15189  metcnp3  15206  logbgcd1irr  15662  gausslemma2dlem1a  15758  gausslemma2dlem2  15762  gausslemma2dlem3  15763  lgsquad2lem2  15782  2lgslem1a1  15786  2sqlem6  15820  umgrnloop  15937  upgredgpr  15968  usgrausgrben  15991  usgredg2vlem2  16042  ushgredgedg  16045  ushgredgedgloop  16047  wlk1walkdom  16131  uspgr2wlkeqi  16139  clwwlk1loop  16168  clwwlkccatlem  16169  umgrclwwlkge2  16171  bj-rspgt  16259