MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  an4s Structured version   Visualization version   GIF version

Theorem an4s 864
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
Hypothesis
Ref Expression
an4s.1 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
an4s (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)

Proof of Theorem an4s
StepHypRef Expression
1 an4 860 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ ((𝜑𝜓) ∧ (𝜒𝜃)))
2 an4s.1 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
31, 2sylbi 205 1 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  an42s  865  anandis  868  anandirs  869  ax13  2232  nfeqf  2285  frminex  5005  trin2  5422  funprg  5837  funcnvqp  5849  fnun  5894  2elresin  5899  f1co  6005  f1oun  6051  f1oco  6054  fvreseq0  6207  f1mpt  6394  poxp  7150  soxp  7151  wfr3g  7274  wfrfun  7286  tfrlem7  7340  oeoe  7540  brecop  7701  pmss12g  7744  dif1en  8052  fiin  8185  tcmin  8474  harval2  8680  genpv  9674  genpdm  9677  genpnnp  9680  genpcd  9681  genpnmax  9682  addcmpblnr  9743  ltsrpr  9751  addclsr  9757  mulclsr  9758  addasssr  9762  mulasssr  9764  distrsr  9765  mulgt0sr  9779  addresr  9812  mulresr  9813  axaddf  9819  axmulf  9820  axaddass  9830  axmulass  9831  axdistr  9832  mulgt0  9963  mul4  10053  add4  10104  2addsub  10143  addsubeq4  10144  sub4  10174  muladd  10310  mulsub  10320  mulge0  10392  add20i  10417  mulge0i  10421  mulne0  10515  divmuldiv  10571  rec11i  10612  ltmul12a  10725  mulge0b  10739  zmulcl  11256  uz2mulcl  11595  qaddcl  11633  qmulcl  11635  qreccl  11637  rpaddcl  11683  xmulgt0  11939  xmulge0  11940  ixxin  12016  ge0addcl  12108  ge0xaddcl  12110  fzadd2  12199  serge0  12669  expge1  12711  sqrmo  13783  rexanuz  13876  amgm2  13900  mulcn2  14117  dvds2ln  14795  opoe  14868  omoe  14869  opeo  14870  omeo  14871  divalglem6  14902  divalglem8  14904  lcmcllem  15090  lcmgcd  15101  lcmdvds  15102  pc2dvds  15364  catpropd  16135  gimco  17476  efgrelexlemb  17929  pf1ind  19483  psgnghm  19687  tgcl  20523  innei  20678  iunconlem  20979  txbas  21119  txss12  21157  txbasval  21158  tx1stc  21202  fbunfip  21422  tsmsxp  21707  blsscls2  22057  bddnghm  22269  qtopbaslem  22301  iimulcl  22472  icoopnst  22474  iocopnst  22475  iccpnfcnv  22479  mumullem2  24620  fsumvma  24652  lgslem3  24738  pntrsumbnd2  24970  ajmoi  26901  hvadd4  27080  hvsub4  27081  shsel3  27361  shscli  27363  shscom  27365  chj4  27581  5oalem3  27702  5oalem5  27704  5oalem6  27705  hoadd4  27830  adjmo  27878  adjsym  27879  cnvadj  27938  leopmuli  28179  mdslmd1lem2  28372  chirredlem2  28437  chirredi  28440  cdjreui  28478  addltmulALT  28492  reofld  28974  xrge0iifcnv  29110  poseq  30797  frr3g  30826  frrlem4  30830  frrlem5c  30833  funtransport  31111  btwnconn1lem13  31179  btwnconn1lem14  31180  outsideofeu  31211  outsidele  31212  funray  31220  lineintmo  31237  icoreclin  32181  poimirlem27  32406  heicant  32414  itg2gt0cn  32435  bndss  32555  isdrngo3  32728  riscer  32757  intidl  32798  unxpwdom3  36483  gbegt5  39985  wlknwwlksnfun  41084
  Copyright terms: Public domain W3C validator