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

Theorem com23 76
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 70 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  77  com13  78  pm2.04  80  pm2.86d  97  impancom  251  con2d  562  impidc  764  pm2.61dc  771  3com23  1119  expcomd  1344  spimth  1637  sbiedh  1684  eqrdav  2053  necon4bbiddc  2292  ralrimdva  2414  ralrimdvva  2419  ceqsalt  2595  vtoclgft  2619  reu6  2750  sbciegft  2813  reuss2  3242  reupick  3246  reusv3  4217  ssrel  4453  ssrel2  4455  ssrelrel  4465  funssres  4967  funcnvuni  4993  fv3  5222  fvmptt  5287  funfvima2  5416  isoini  5482  isopolem  5486  f1ocnv2d  5729  f1o2ndf1  5874  nnmordi  6117  nnmord  6118  xpdom2  6333  findcard2  6374  findcard2s  6375  findcard2d  6376  findcard2sd  6377  ordiso2  6385  genpcdl  6645  genpcuu  6646  distrlem5prl  6712  distrlem5pru  6713  lemul12a  7873  divgt0  7883  divge0  7884  bndndx  8208  elnnz  8282  nzadd  8324  fzind  8382  fnn0ind  8383  eqreznegel  8616  lbzbi  8618  irradd  8648  irrmul  8649  ledivge1le  8720  iccid  8865  uzsubsubfz  8983  fzrevral  9039  elfz0fzfz0  9055  fz0fzelfz0  9056  elfzmlbp  9062  elfzodifsumelfzo  9129  ssfzo12bi  9153  elfzonelfzo  9158  flqeqceilz  9233  le2sq2  9460  facdiv  9570  facwordi  9572  faclbnd  9573  cau3lem  9904  mulcn2  10027  climcau  10060  climcaucn  10064  dvdsdivcl  10125  ltoddhalfle  10168  halfleoddlt  10169  bj-rspgt  10255
  Copyright terms: Public domain W3C validator