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  4551  ssrel  4807  ssrel2  4809  ssrelrel  4819  ssrelrn  4914  funssres  5360  funcnvuni  5390  fv3  5652  fvmptt  5728  funfvima2  5876  isoini  5948  isopolem  5952  f1ocnv2d  6216  f1o2ndf1  6380  nnmordi  6670  nnmord  6671  xpdom2  6998  findcard2  7059  findcard2s  7060  findcard2d  7061  findcard2sd  7062  xpfi  7102  ordiso2  7210  updjud  7257  genpcdl  7714  genpcuu  7715  distrlem5prl  7781  distrlem5pru  7782  lemul12a  9017  divgt0  9027  divge0  9028  lbreu  9100  bndndx  9376  elnnz  9464  nzadd  9507  fzind  9570  fnn0ind  9571  eqreznegel  9817  lbzbi  9819  irradd  9849  irrmul  9850  ledivge1le  9930  iccid  10129  uzsubsubfz  10251  fzrevral  10309  elfz0fzfz0  10330  fz0fzelfz0  10331  elfzmlbp  10336  elincfzoext  10407  elfzodifsumelfzo  10415  ssfzo12bi  10439  elfzonelfzo  10444  flqeqceilz  10548  le2sq2  10845  facdiv  10968  facwordi  10970  faclbnd  10971  fundm2domnop0  11075  swrdswrdlem  11244  swrdswrd  11245  ccatopth2  11257  wrd2ind  11263  pfxccatin12lem2a  11267  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccatin12lem3  11272  swrdccat  11275  swrdccat3blem  11279  reuccatpfxs1lem  11286  cau3lem  11633  mulcn2  11831  climcau  11866  climcaucn  11870  modfsummod  11977  p1modz1  12313  dvdsdivcl  12369  ltoddhalfle  12412  halfleoddlt  12413  ndvdssub  12449  dfgcd2  12543  coprmdvds1  12621  coprmdvds  12622  coprmdvds2  12623  divgcdcoprm0  12631  cncongr1  12633  cncongr2  12634  prmfac1  12682  pcqcl  12837  dvdsprmpweqle  12868  oddprmdvds  12885  prmpwdvds  12886  infpnlem1  12890  lidrididd  13423  mulgaddcom  13691  mulginvcom  13692  imasabl  13881  lmodfopnelem1  14296  lss1d  14355  rnglidlmcl  14452  znrrg  14632  uniopn  14683  tgcnp  14891  iscnp4  14900  lmtopcnp  14932  txlm  14961  metss  15176  metcnp3  15193  logbgcd1irr  15649  gausslemma2dlem1a  15745  gausslemma2dlem2  15749  gausslemma2dlem3  15750  lgsquad2lem2  15769  2lgslem1a1  15773  2sqlem6  15807  umgrnloop  15924  upgredgpr  15955  usgrausgrben  15978  usgredg2vlem2  16029  ushgredgedg  16032  ushgredgedgloop  16034  wlk1walkdom  16080  uspgr2wlkeqi  16088  bj-rspgt  16174