ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  com23 GIF 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 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
com23 (𝜑 → (𝜒 → (𝜓𝜃)))

Proof of Theorem com23
StepHypRef Expression
1 com3.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 pm2.27 39 . 2 (𝜒 → ((𝜒𝜃) → 𝜃))
31, 2syl9 71 1 (𝜑 → (𝜒 → (𝜓𝜃)))
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  a2and  525  con2d  589  impidc  793  pm2.61dc  800  3com23  1149  expcomd  1375  spimth  1670  sbiedh  1717  eqrdav  2087  necon4bbiddc  2329  ralrimdva  2453  ralrimdvva  2458  ceqsalt  2645  vtoclgft  2669  reu6  2804  sbciegft  2869  reuss2  3279  reupick  3283  reusv3  4282  ssrel  4526  ssrel2  4528  ssrelrel  4538  funssres  5056  funcnvuni  5083  fv3  5328  fvmptt  5394  funfvima2  5527  isoini  5597  isopolem  5601  f1ocnv2d  5848  f1o2ndf1  5993  nnmordi  6273  nnmord  6274  xpdom2  6545  findcard2  6603  findcard2s  6604  findcard2d  6605  findcard2sd  6606  xpfi  6638  ordiso2  6726  updjud  6771  genpcdl  7076  genpcuu  7077  distrlem5prl  7143  distrlem5pru  7144  lemul12a  8321  divgt0  8331  divge0  8332  lbreu  8404  bndndx  8670  elnnz  8758  nzadd  8800  fzind  8859  fnn0ind  8860  eqreznegel  9097  lbzbi  9099  irradd  9129  irrmul  9130  ledivge1le  9201  iccid  9341  uzsubsubfz  9459  fzrevral  9515  elfz0fzfz0  9533  fz0fzelfz0  9534  elfzmlbp  9539  elfzodifsumelfzo  9608  ssfzo12bi  9632  elfzonelfzo  9637  flqeqceilz  9721  le2sq2  10026  facdiv  10142  facwordi  10144  faclbnd  10145  cau3lem  10543  mulcn2  10697  climcau  10732  climcaucn  10736  modfsummod  10848  dvdsdivcl  11125  ltoddhalfle  11167  halfleoddlt  11168  ndvdssub  11204  dfgcd2  11277  coprmdvds1  11347  coprmdvds  11348  coprmdvds2  11349  divgcdcoprm0  11357  cncongr1  11359  cncongr2  11360  prmfac1  11405  uniopn  11553  bj-rspgt  11641
  Copyright terms: Public domain W3C validator