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  560  con2d  629  impidc  866  pm2.61dc  873  3com23  1236  expcomd  1487  spimth  1784  sbiedh  1836  eqrdav  2233  necon4bbiddc  2488  ralrimdva  2624  ralrimdvva  2629  ceqsalt  2842  vtoclgft  2867  reu6  3009  sbciegft  3076  reuss2  3505  reupick  3509  reusv3  4586  ssrel  4843  ssrel2  4845  ssrelrel  4855  ssrelrn  4952  funssres  5400  funcnvuni  5430  f1ssf1  5651  fv3  5698  fvmptt  5774  funfvima2  5924  isoini  5997  isopolem  6001  f1ocnv2d  6267  f1o3d  6271  f1o2ndf1  6437  suppfnss  6470  suppssdc  6473  nnmordi  6762  nnmord  6763  xpdom2  7095  findcard2  7159  findcard2s  7160  findcard2d  7161  findcard2sd  7162  xpfi  7205  ordiso2  7339  updjud  7386  genpcdl  7850  genpcuu  7851  distrlem5prl  7917  distrlem5pru  7918  lemul12a  9156  divgt0  9166  divge0  9167  lbreu  9239  bndndx  9515  elnnz  9607  nzadd  9650  fzind  9714  fnn0ind  9715  eqreznegel  9967  lbzbi  9969  irradd  9999  irrmul  10000  ledivge1le  10080  iccid  10280  uzsubsubfz  10404  fzrevral  10464  elfz0fzfz0  10485  fz0fzelfz0  10486  elfzmlbp  10491  elincfzoext  10563  elfzodifsumelfzo  10571  ssfzo12bi  10595  elfzonelfzo  10600  flqeqceilz  10707  le2sq2  11004  facdiv  11128  facwordi  11130  faclbnd  11131  fundm2domnop0  11248  swrdswrdlem  11424  swrdswrd  11425  ccatopth2  11437  wrd2ind  11443  pfxccatin12lem2a  11447  swrdccatin2  11449  pfxccatin12lem2  11451  pfxccatin12lem3  11452  swrdccat  11455  swrdccat3blem  11459  reuccatpfxs1lem  11466  cau3lem  11828  mulcn2  12026  climcau  12061  climcaucn  12065  modfsummod  12173  p1modz1  12509  dvdsdivcl  12565  ltoddhalfle  12608  halfleoddlt  12609  ndvdssub  12645  dfgcd2  12739  coprmdvds1  12817  coprmdvds  12818  coprmdvds2  12819  divgcdcoprm0  12827  cncongr1  12829  cncongr2  12830  prmfac1  12878  pcqcl  13033  dvdsprmpweqle  13064  oddprmdvds  13081  prmpwdvds  13082  infpnlem1  13086  lidrididd  13649  mulgaddcom  13903  mulginvcom  13904  imasabl  14093  gfsumval  14106  lmodfopnelem1  14602  lss1d  14661  rnglidlmcl  14758  znrrg  14938  uniopn  14996  tgcnp  15204  iscnp4  15213  lmtopcnp  15245  txlm  15274  metss  15489  metcnp3  15506  logbgcd1irr  15962  gausslemma2dlem1a  16061  gausslemma2dlem2  16065  gausslemma2dlem3  16066  lgsquad2lem2  16085  2lgslem1a1  16089  2sqlem6  16123  umgrnloop  16241  upgredgpr  16274  usgrausgrben  16297  usgredg2vlem2  16348  ushgredgedg  16351  ushgredgedgloop  16353  wlk1walkdom  16484  uspgr2wlkeqi  16492  clwwlk1loop  16524  clwwlkccatlem  16525  umgrclwwlkge2  16527  clwwlknonex2lem2  16563  clwwlknonex2  16564  lealltlt2  16636  bj-rspgt  16698