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  9153  divgt0  9163  divge0  9164  lbreu  9236  bndndx  9512  elnnz  9604  nzadd  9647  fzind  9711  fnn0ind  9712  eqreznegel  9964  lbzbi  9966  irradd  9996  irrmul  9997  ledivge1le  10077  iccid  10277  uzsubsubfz  10401  fzrevral  10461  elfz0fzfz0  10482  fz0fzelfz0  10483  elfzmlbp  10488  elincfzoext  10560  elfzodifsumelfzo  10568  ssfzo12bi  10592  elfzonelfzo  10597  flqeqceilz  10704  le2sq2  11001  facdiv  11125  facwordi  11127  faclbnd  11128  fundm2domnop0  11245  swrdswrdlem  11421  swrdswrd  11422  ccatopth2  11434  wrd2ind  11440  pfxccatin12lem2a  11444  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12lem3  11449  swrdccat  11452  swrdccat3blem  11456  reuccatpfxs1lem  11463  cau3lem  11824  mulcn2  12022  climcau  12057  climcaucn  12061  modfsummod  12169  p1modz1  12505  dvdsdivcl  12561  ltoddhalfle  12604  halfleoddlt  12605  ndvdssub  12641  dfgcd2  12735  coprmdvds1  12813  coprmdvds  12814  coprmdvds2  12815  divgcdcoprm0  12823  cncongr1  12825  cncongr2  12826  prmfac1  12874  pcqcl  13029  dvdsprmpweqle  13060  oddprmdvds  13077  prmpwdvds  13078  infpnlem1  13082  lidrididd  13679  mulgaddcom  13947  mulginvcom  13948  imasabl  14137  lmodfopnelem1  14584  lss1d  14643  rnglidlmcl  14740  znrrg  14920  uniopn  14978  tgcnp  15186  iscnp4  15195  lmtopcnp  15227  txlm  15256  metss  15471  metcnp3  15488  logbgcd1irr  15944  gausslemma2dlem1a  16043  gausslemma2dlem2  16047  gausslemma2dlem3  16048  lgsquad2lem2  16067  2lgslem1a1  16071  2sqlem6  16105  umgrnloop  16223  upgredgpr  16256  usgrausgrben  16279  usgredg2vlem2  16330  ushgredgedg  16333  ushgredgedgloop  16335  wlk1walkdom  16466  uspgr2wlkeqi  16474  clwwlk1loop  16506  clwwlkccatlem  16507  umgrclwwlkge2  16509  clwwlknonex2lem2  16545  clwwlknonex2  16546  bj-rspgt  16670  gfsumval  16974