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

Theorem an4s 642
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 638 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ ((𝜑𝜓) ∧ (𝜒𝜃)))
2 an4s.1 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
31, 2sylbi 208 1 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  an42s  643  anandis  660  anandirs  661  ax13  2425  nfeqf  2471  frminex  5288  trin2  5727  funprg  6151  funcnvqp  6161  fnun  6205  2elresin  6210  f1co  6323  f1oun  6369  f1oco  6372  fvreseq0  6536  f1mpt  6739  poxp  7520  soxp  7521  wfr3g  7645  wfrfun  7658  tfrlem7  7712  oeoe  7913  brecop  8072  pmss12g  8116  dif1en  8429  fiin  8564  tcmin  8861  harval2  9103  genpv  10103  genpdm  10106  genpnnp  10109  genpcd  10110  genpnmax  10111  addcmpblnr  10172  ltsrpr  10180  addclsr  10186  mulclsr  10187  addasssr  10191  mulasssr  10193  distrsr  10194  mulgt0sr  10208  addresr  10241  mulresr  10242  axaddf  10248  axmulf  10249  axaddass  10259  axmulass  10260  axdistr  10261  mulgt0  10397  mul4  10487  add4  10538  2addsub  10577  addsubeq4  10578  sub4  10608  muladd  10744  mulsub  10755  mulge0  10828  add20i  10853  mulge0i  10857  mulne0  10951  divmuldiv  11007  rec11i  11048  ltmul12a  11161  mulge0b  11175  zmulcl  11688  uz2mulcl  11981  qaddcl  12019  qmulcl  12021  qreccl  12023  rpaddcl  12064  xmulgt0  12327  xmulge0  12328  ixxin  12406  ge0addcl  12500  ge0xaddcl  12502  fzadd2  12595  serge0  13074  expge1  13116  sqrmo  14211  rexanuz  14304  amgm2  14328  mulcn2  14545  dvds2ln  15233  opoe  15303  omoe  15304  opeo  15305  omeo  15306  divalglem6  15337  divalglem8  15339  lcmcllem  15524  lcmgcd  15535  lcmdvds  15536  pc2dvds  15796  catpropd  16569  gimco  17908  efgrelexlemb  18360  pf1ind  19923  psgnghm  20129  tgcl  20983  innei  21139  iunconnlem  21440  txbas  21580  txss12  21618  txbasval  21619  tx1stc  21663  fbunfip  21882  tsmsxp  22167  blsscls2  22518  bddnghm  22739  qtopbaslem  22771  iimulcl  22945  icoopnst  22947  iocopnst  22948  iccpnfcnv  22952  mumullem2  25116  fsumvma  25148  lgslem3  25234  pntrsumbnd2  25466  wlknwwlksnfunOLD  27011  ajmoi  28039  hvadd4  28218  hvsub4  28219  shsel3  28499  shscli  28501  shscom  28503  chj4  28719  5oalem3  28840  5oalem5  28842  5oalem6  28843  hoadd4  28968  adjmo  29016  adjsym  29017  cnvadj  29076  leopmuli  29317  mdslmd1lem2  29510  chirredlem2  29575  chirredi  29578  cdjreui  29616  addltmulALT  29630  reofld  30162  xrge0iifcnv  30301  poseq  32071  frr3g  32097  frrlem5c  32104  funtransport  32456  btwnconn1lem13  32524  btwnconn1lem14  32525  outsideofeu  32556  outsidele  32557  funray  32565  lineintmo  32582  icoreclin  33518  poimirlem27  33746  heicant  33754  itg2gt0cn  33774  bndss  33893  isdrngo3  34066  riscer  34095  intidl  34136  unxpwdom3  38163  gbegt5  42221
  Copyright terms: Public domain W3C validator