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  99  impcomd  253  impancom  258  a2and  530  con2d  596  impidc  826  pm2.61dc  833  3com23  1170  expcomd  1400  spimth  1696  sbiedh  1743  eqrdav  2114  necon4bbiddc  2357  ralrimdva  2487  ralrimdvva  2492  ceqsalt  2684  vtoclgft  2708  reu6  2844  sbciegft  2909  reuss2  3324  reupick  3328  reusv3  4349  ssrel  4595  ssrel2  4597  ssrelrel  4607  funssres  5133  funcnvuni  5160  fv3  5410  fvmptt  5478  funfvima2  5616  isoini  5685  isopolem  5689  f1ocnv2d  5940  f1o2ndf1  6091  nnmordi  6378  nnmord  6379  xpdom2  6691  findcard2  6749  findcard2s  6750  findcard2d  6751  findcard2sd  6752  xpfi  6784  ordiso2  6886  updjud  6933  genpcdl  7291  genpcuu  7292  distrlem5prl  7358  distrlem5pru  7359  lemul12a  8580  divgt0  8590  divge0  8591  lbreu  8663  bndndx  8930  elnnz  9018  nzadd  9060  fzind  9120  fnn0ind  9121  eqreznegel  9358  lbzbi  9360  irradd  9390  irrmul  9391  ledivge1le  9464  iccid  9659  uzsubsubfz  9778  fzrevral  9836  elfz0fzfz0  9854  fz0fzelfz0  9855  elfzmlbp  9860  elfzodifsumelfzo  9929  ssfzo12bi  9953  elfzonelfzo  9958  flqeqceilz  10042  le2sq2  10319  facdiv  10435  facwordi  10437  faclbnd  10438  cau3lem  10837  mulcn2  11032  climcau  11067  climcaucn  11071  modfsummod  11178  dvdsdivcl  11455  ltoddhalfle  11497  halfleoddlt  11498  ndvdssub  11534  dfgcd2  11609  coprmdvds1  11679  coprmdvds  11680  coprmdvds2  11681  divgcdcoprm0  11689  cncongr1  11691  cncongr2  11692  prmfac1  11737  uniopn  12074  tgcnp  12284  iscnp4  12293  lmtopcnp  12325  txlm  12354  metss  12569  metcnp3  12586  bj-rspgt  12827
  Copyright terms: Public domain W3C validator