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

Theorem an4s 659
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 655 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ ((𝜑𝜓) ∧ (𝜒𝜃)))
2 an4s.1 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
31, 2sylbi 216 1 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  an42s  660  anandis  677  anandirs  678  ax13  2374  nfeqf  2380  frminex  5614  trin2  6078  funprg  6556  funcnvqp  6566  fnun  6615  2elresin  6623  f1cof1  6750  f1coOLD  6752  f1oun  6804  f1oco  6808  fvreseq0  6989  f1mpt  7209  poxp  8061  soxp  8062  poseq  8091  wfr3g  8254  wfrfunOLD  8266  tfrlem7  8330  oeoe  8547  brecop  8750  pmss12g  8808  dif1ennnALT  9222  fiin  9359  tcmin  9678  frr3g  9693  harval2  9934  genpv  10936  genpdm  10939  genpnnp  10942  genpcd  10943  genpnmax  10944  addcmpblnr  11006  ltsrpr  11014  addclsr  11020  mulclsr  11021  addasssr  11025  mulasssr  11027  distrsr  11028  mulgt0sr  11042  addresr  11075  mulresr  11076  axaddf  11082  axmulf  11083  axaddass  11093  axmulass  11094  axdistr  11095  mulgt0  11233  mul4  11324  add4  11376  2addsub  11416  addsubeq4  11417  sub4  11447  muladd  11588  mulsub  11599  mulge0  11674  add20i  11699  mulge0i  11703  mulne0  11798  divmuldiv  11856  rec11i  11897  ltmul12a  12012  mulge0b  12026  zmulcl  12553  uz2mulcl  12852  qaddcl  12891  qmulcl  12893  qreccl  12895  rpaddcl  12938  xmulgt0  13203  xmulge0  13204  ixxin  13282  ge0addcl  13378  ge0xaddcl  13380  fzadd2  13477  serge0  13963  expge1  14006  sqrmo  15137  rexanuz  15231  amgm2  15255  bhmafibid1cn  15349  bhmafibid2cn  15350  mulcn2  15479  dvds2ln  16172  opoe  16246  omoe  16247  opeo  16248  omeo  16249  divalglem6  16281  divalglem8  16283  lcmcllem  16473  lcmgcd  16484  lcmdvds  16485  pc2dvds  16752  catpropd  17590  gimco  19059  efgrelexlemb  19533  psgnghm  20987  pf1ind  21724  tgcl  22322  innei  22479  iunconnlem  22781  txbas  22921  txss12  22959  txbasval  22960  tx1stc  23004  fbunfip  23223  tsmsxp  23509  blsscls2  23863  bddnghm  24093  qtopbaslem  24125  iimulcl  24303  icoopnst  24305  iocopnst  24306  iccpnfcnv  24310  mumullem2  26532  fsumvma  26564  lgslem3  26650  pntrsumbnd2  26918  ajmoi  29803  hvadd4  29981  hvsub4  29982  shsel3  30260  shscli  30262  shscom  30264  chj4  30480  5oalem3  30601  5oalem5  30603  5oalem6  30604  hoadd4  30729  adjmo  30777  adjsym  30778  cnvadj  30837  leopmuli  31078  mdslmd1lem2  31271  chirredlem2  31336  chirredi  31339  cdjreui  31377  addltmulALT  31391  reofld  32139  xrge0iifcnv  32517  funtransport  34619  btwnconn1lem13  34687  btwnconn1lem14  34688  outsideofeu  34719  outsidele  34720  funray  34728  lineintmo  34745  bj-nnfan  35216  bj-nnfor  35218  icoreclin  35831  poimirlem27  36108  heicant  36116  itg2gt0cn  36136  bndss  36248  isdrngo3  36421  riscer  36450  intidl  36491  rimco  40702  unxpwdom3  41425  gbegt5  45960
  Copyright terms: Public domain W3C validator