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

Theorem an4s 869
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 865 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ ((𝜑𝜓) ∧ (𝜒𝜃)))
2 an4s.1 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
31, 2sylbi 207 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 197  df-an 386
This theorem is referenced by:  an42s  870  anandis  873  anandirs  874  ax13  2248  nfeqf  2300  frminex  5092  trin2  5517  funprg  5938  funcnvqp  5950  fnun  5995  2elresin  6000  f1co  6108  f1oun  6154  f1oco  6157  fvreseq0  6315  f1mpt  6515  poxp  7286  soxp  7287  wfr3g  7410  wfrfun  7422  tfrlem7  7476  oeoe  7676  brecop  7837  pmss12g  7881  dif1en  8190  fiin  8325  tcmin  8614  harval2  8820  genpv  9818  genpdm  9821  genpnnp  9824  genpcd  9825  genpnmax  9826  addcmpblnr  9887  ltsrpr  9895  addclsr  9901  mulclsr  9902  addasssr  9906  mulasssr  9908  distrsr  9909  mulgt0sr  9923  addresr  9956  mulresr  9957  axaddf  9963  axmulf  9964  axaddass  9974  axmulass  9975  axdistr  9976  mulgt0  10112  mul4  10202  add4  10253  2addsub  10292  addsubeq4  10293  sub4  10323  muladd  10459  mulsub  10470  mulge0  10543  add20i  10568  mulge0i  10572  mulne0  10666  divmuldiv  10722  rec11i  10763  ltmul12a  10876  mulge0b  10890  zmulcl  11423  uz2mulcl  11763  qaddcl  11801  qmulcl  11803  qreccl  11805  rpaddcl  11851  xmulgt0  12110  xmulge0  12111  ixxin  12189  ge0addcl  12281  ge0xaddcl  12283  fzadd2  12373  serge0  12850  expge1  12892  sqrmo  13986  rexanuz  14079  amgm2  14103  mulcn2  14320  dvds2ln  15008  opoe  15081  omoe  15082  opeo  15083  omeo  15084  divalglem6  15115  divalglem8  15117  lcmcllem  15303  lcmgcd  15314  lcmdvds  15315  pc2dvds  15577  catpropd  16363  gimco  17704  efgrelexlemb  18157  pf1ind  19713  psgnghm  19920  tgcl  20767  innei  20923  iunconnlem  21224  txbas  21364  txss12  21402  txbasval  21403  tx1stc  21447  fbunfip  21667  tsmsxp  21952  blsscls2  22303  bddnghm  22524  qtopbaslem  22556  iimulcl  22730  icoopnst  22732  iocopnst  22733  iccpnfcnv  22737  mumullem2  24900  fsumvma  24932  lgslem3  25018  pntrsumbnd2  25250  wlknwwlksnfun  26768  ajmoi  27698  hvadd4  27877  hvsub4  27878  shsel3  28158  shscli  28160  shscom  28162  chj4  28378  5oalem3  28499  5oalem5  28501  5oalem6  28502  hoadd4  28627  adjmo  28675  adjsym  28676  cnvadj  28735  leopmuli  28976  mdslmd1lem2  29169  chirredlem2  29234  chirredi  29237  cdjreui  29275  addltmulALT  29289  reofld  29825  xrge0iifcnv  29964  poseq  31734  frr3g  31763  frrlem4  31767  frrlem5c  31770  funtransport  32122  btwnconn1lem13  32190  btwnconn1lem14  32191  outsideofeu  32222  outsidele  32223  funray  32231  lineintmo  32248  icoreclin  33185  poimirlem27  33416  heicant  33424  itg2gt0cn  33445  bndss  33565  isdrngo3  33738  riscer  33767  intidl  33808  unxpwdom3  37491  gbegt5  41420
  Copyright terms: Public domain W3C validator