ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  com23 Unicode version

Theorem com23 77
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  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
com23  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )

Proof of Theorem com23
StepHypRef Expression
1 com3.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
2 pm2.27 39 . 2  |-  ( ch 
->  ( ( ch  ->  th )  ->  th )
)
31, 2syl9 71 1  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  com3r  78  com13  79  pm2.04  81  pm2.86d  98  impancom  256  con2d  587  impidc  791  pm2.61dc  798  3com23  1147  expcomd  1373  spimth  1667  sbiedh  1714  eqrdav  2084  necon4bbiddc  2325  ralrimdva  2449  ralrimdvva  2454  ceqsalt  2639  vtoclgft  2663  reu6  2795  sbciegft  2858  reuss2  3268  reupick  3272  reusv3  4256  ssrel  4494  ssrel2  4496  ssrelrel  4506  funssres  5021  funcnvuni  5048  fv3  5291  fvmptt  5357  funfvima2  5488  isoini  5558  isopolem  5562  f1ocnv2d  5805  f1o2ndf1  5950  nnmordi  6227  nnmord  6228  xpdom2  6499  findcard2  6557  findcard2s  6558  findcard2d  6559  findcard2sd  6560  xpfi  6590  ordiso2  6672  updjud  6717  genpcdl  7022  genpcuu  7023  distrlem5prl  7089  distrlem5pru  7090  lemul12a  8258  divgt0  8268  divge0  8269  lbreu  8341  bndndx  8605  elnnz  8693  nzadd  8735  fzind  8794  fnn0ind  8795  eqreznegel  9031  lbzbi  9033  irradd  9063  irrmul  9064  ledivge1le  9135  iccid  9275  uzsubsubfz  9393  fzrevral  9449  elfz0fzfz0  9465  fz0fzelfz0  9466  elfzmlbp  9471  elfzodifsumelfzo  9540  ssfzo12bi  9564  elfzonelfzo  9569  flqeqceilz  9653  le2sq2  9928  facdiv  10042  facwordi  10044  faclbnd  10045  cau3lem  10442  mulcn2  10593  climcau  10626  climcaucn  10630  dvdsdivcl  10726  ltoddhalfle  10768  halfleoddlt  10769  ndvdssub  10805  dfgcd2  10878  coprmdvds1  10948  coprmdvds  10949  coprmdvds2  10950  divgcdcoprm0  10958  cncongr1  10960  cncongr2  10961  prmfac1  11006  bj-rspgt  11124
  Copyright terms: Public domain W3C validator