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  con2d  587  impidc  789  pm2.61dc  796  3com23  1145  expcomd  1371  spimth  1664  sbiedh  1711  eqrdav  2081  necon4bbiddc  2320  ralrimdva  2442  ralrimdvva  2447  ceqsalt  2626  vtoclgft  2650  reu6  2782  sbciegft  2845  reuss2  3251  reupick  3255  reusv3  4218  ssrel  4454  ssrel2  4456  ssrelrel  4466  funssres  4972  funcnvuni  4999  fv3  5229  fvmptt  5294  funfvima2  5423  isoini  5488  isopolem  5492  f1ocnv2d  5735  f1o2ndf1  5880  nnmordi  6155  nnmord  6156  xpdom2  6375  findcard2  6423  findcard2s  6424  findcard2d  6425  findcard2sd  6426  ordiso2  6505  genpcdl  6771  genpcuu  6772  distrlem5prl  6838  distrlem5pru  6839  lemul12a  8007  divgt0  8017  divge0  8018  lbreu  8090  bndndx  8354  elnnz  8442  nzadd  8484  fzind  8543  fnn0ind  8544  eqreznegel  8780  lbzbi  8782  irradd  8812  irrmul  8813  ledivge1le  8884  iccid  9024  uzsubsubfz  9142  fzrevral  9198  elfz0fzfz0  9214  fz0fzelfz0  9215  elfzmlbp  9220  elfzodifsumelfzo  9287  ssfzo12bi  9311  elfzonelfzo  9316  flqeqceilz  9400  le2sq2  9648  facdiv  9762  facwordi  9764  faclbnd  9765  cau3lem  10138  mulcn2  10289  climcau  10322  climcaucn  10326  dvdsdivcl  10395  ltoddhalfle  10437  halfleoddlt  10438  ndvdssub  10474  dfgcd2  10547  coprmdvds1  10617  coprmdvds  10618  coprmdvds2  10619  divgcdcoprm0  10627  cncongr1  10629  cncongr2  10630  prmfac1  10675  bj-rspgt  10747
 Copyright terms: Public domain W3C validator