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  99  impcomd  253  impancom  258  a2and  548  con2d  614  impidc  848  pm2.61dc  855  3com23  1199  expcomd  1429  spimth  1723  sbiedh  1775  eqrdav  2164  necon4bbiddc  2409  ralrimdva  2545  ralrimdvva  2550  ceqsalt  2751  vtoclgft  2775  reu6  2914  sbciegft  2980  reuss2  3401  reupick  3405  reusv3  4437  ssrel  4691  ssrel2  4693  ssrelrel  4703  funssres  5229  funcnvuni  5256  fv3  5508  fvmptt  5576  funfvima2  5716  isoini  5785  isopolem  5789  f1ocnv2d  6041  f1o2ndf1  6192  nnmordi  6480  nnmord  6481  xpdom2  6793  findcard2  6851  findcard2s  6852  findcard2d  6853  findcard2sd  6854  xpfi  6891  ordiso2  6996  updjud  7043  genpcdl  7456  genpcuu  7457  distrlem5prl  7523  distrlem5pru  7524  lemul12a  8753  divgt0  8763  divge0  8764  lbreu  8836  bndndx  9109  elnnz  9197  nzadd  9239  fzind  9302  fnn0ind  9303  eqreznegel  9548  lbzbi  9550  irradd  9580  irrmul  9581  ledivge1le  9658  iccid  9857  uzsubsubfz  9978  fzrevral  10036  elfz0fzfz0  10057  fz0fzelfz0  10058  elfzmlbp  10063  elfzodifsumelfzo  10132  ssfzo12bi  10156  elfzonelfzo  10161  flqeqceilz  10249  le2sq2  10526  facdiv  10647  facwordi  10649  faclbnd  10650  cau3lem  11052  mulcn2  11249  climcau  11284  climcaucn  11288  modfsummod  11395  p1modz1  11730  dvdsdivcl  11784  ltoddhalfle  11826  halfleoddlt  11827  ndvdssub  11863  dfgcd2  11943  coprmdvds1  12019  coprmdvds  12020  coprmdvds2  12021  divgcdcoprm0  12029  cncongr1  12031  cncongr2  12032  prmfac1  12080  pcqcl  12234  dvdsprmpweqle  12264  oddprmdvds  12280  prmpwdvds  12281  infpnlem1  12285  uniopn  12599  tgcnp  12809  iscnp4  12818  lmtopcnp  12850  txlm  12879  metss  13094  metcnp3  13111  logbgcd1irr  13485  2sqlem6  13556  bj-rspgt  13627