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

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
StepHypRef Expression
1 com3.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 pm2.27 40 . 2 (𝜒 → ((𝜒𝜃) → 𝜃))
31, 2syl9 72 1 (𝜑 → (𝜒 → (𝜓𝜃)))
Colors of variables: wff set class
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  558  con2d  625  impidc  859  pm2.61dc  866  3com23  1211  expcomd  1452  spimth  1746  sbiedh  1798  eqrdav  2192  necon4bbiddc  2438  ralrimdva  2574  ralrimdvva  2579  ceqsalt  2786  vtoclgft  2811  reu6  2950  sbciegft  3017  reuss2  3440  reupick  3444  reusv3  4492  ssrel  4748  ssrel2  4750  ssrelrel  4760  funssres  5297  funcnvuni  5324  fv3  5578  fvmptt  5650  funfvima2  5792  isoini  5862  isopolem  5866  f1ocnv2d  6124  f1o2ndf1  6283  nnmordi  6571  nnmord  6572  xpdom2  6887  findcard2  6947  findcard2s  6948  findcard2d  6949  findcard2sd  6950  xpfi  6988  ordiso2  7096  updjud  7143  genpcdl  7581  genpcuu  7582  distrlem5prl  7648  distrlem5pru  7649  lemul12a  8883  divgt0  8893  divge0  8894  lbreu  8966  bndndx  9242  elnnz  9330  nzadd  9372  fzind  9435  fnn0ind  9436  eqreznegel  9682  lbzbi  9684  irradd  9714  irrmul  9715  ledivge1le  9795  iccid  9994  uzsubsubfz  10116  fzrevral  10174  elfz0fzfz0  10195  fz0fzelfz0  10196  elfzmlbp  10201  elfzodifsumelfzo  10271  ssfzo12bi  10295  elfzonelfzo  10300  flqeqceilz  10392  le2sq2  10689  facdiv  10812  facwordi  10814  faclbnd  10815  cau3lem  11261  mulcn2  11458  climcau  11493  climcaucn  11497  modfsummod  11604  p1modz1  11940  dvdsdivcl  11995  ltoddhalfle  12037  halfleoddlt  12038  ndvdssub  12074  dfgcd2  12154  coprmdvds1  12232  coprmdvds  12233  coprmdvds2  12234  divgcdcoprm0  12242  cncongr1  12244  cncongr2  12245  prmfac1  12293  pcqcl  12447  dvdsprmpweqle  12478  oddprmdvds  12495  prmpwdvds  12496  infpnlem1  12500  lidrididd  12968  mulgaddcom  13219  mulginvcom  13220  imasabl  13409  lmodfopnelem1  13823  lss1d  13882  rnglidlmcl  13979  znrrg  14159  uniopn  14180  tgcnp  14388  iscnp4  14397  lmtopcnp  14429  txlm  14458  metss  14673  metcnp3  14690  logbgcd1irr  15140  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  gausslemma2dlem3  15220  lgsquad2lem2  15239  2lgslem1a1  15243  2sqlem6  15277  bj-rspgt  15348
  Copyright terms: Public domain W3C validator