Theorem an4s 660

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

Step	Hyp	Ref	Expression
1		an4 656	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 217	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an42s  661  anandis  678  anandirs  679  ax13  2374  nfeqf  2380  frminex  5620  trin2  6099  funprg  6573  funcnvqp  6583  fnun  6635  2elresin  6642  f1cof1  6769  f1oun  6822  f1oco  6826  fvreseq0  7013  f1mpt  7239  poxp  8110  soxp  8111  poseq  8140  wfr3g  8301  tfrlem7  8354  oeoe  8566  brecop  8786  pmss12g  8845  dif1ennnALT  9229  fiin  9380  tcmin  9701  frr3g  9716  harval2  9957  genpv  10959  genpdm  10962  genpnnp  10965  genpcd  10966  genpnmax  10967  addcmpblnr  11029  ltsrpr  11037  addclsr  11043  mulclsr  11044  addasssr  11048  mulasssr  11050  distrsr  11051  mulgt0sr  11065  addresr  11098  mulresr  11099  axaddf  11105  axmulf  11106  axaddass  11116  axmulass  11117  axdistr  11118  mulgt0  11258  mul4  11349  add4  11402  2addsub  11442  addsubeq4  11443  sub4  11474  muladd  11617  mulsub  11628  mulge0  11703  add20i  11728  mulge0i  11732  mulne0  11827  divmuldiv  11889  rec11i  11930  ltmul12a  12045  mulge0b  12060  zmulcl  12589  uz2mulcl  12892  qaddcl  12931  qmulcl  12933  qreccl  12935  rpaddcl  12982  xmulgt0  13250  xmulge0  13251  ixxin  13330  ge0addcl  13428  ge0xaddcl  13430  fzadd2  13527  serge0  14028  expge1  14071  sqrmo  15224  rexanuz  15319  amgm2  15343  bhmafibid1cn  15439  bhmafibid2cn  15440  mulcn2  15569  dvds2ln  16266  opoe  16340  omoe  16341  opeo  16342  omeo  16343  divalglem6  16375  divalglem8  16377  lcmcllem  16573  lcmgcd  16584  lcmdvds  16585  pc2dvds  16857  catpropd  17677  gimco  19207  efgrelexlemb  19687  psgnghm  21496  pf1ind  22249  tgcl  22863  innei  23019  iunconnlem  23321  txbas  23461  txss12  23499  txbasval  23500  tx1stc  23544  fbunfip  23763  tsmsxp  24049  blsscls2  24399  bddnghm  24621  qtopbaslem  24653  iimulcl  24840  icoopnst  24843  iocopnst  24844  iccpnfcnv  24849  mumullem2  27097  fsumvma  27131  lgslem3  27217  pntrsumbnd2  27485  mulsuniflem  28059  readdscl  28357  remulscllem2  28359  remulscl  28360  ajmoi  30794  hvadd4  30972  hvsub4  30973  shsel3  31251  shscli  31253  shscom  31255  chj4  31471  5oalem3  31592  5oalem5  31594  5oalem6  31595  hoadd4  31720  adjmo  31768  adjsym  31769  cnvadj  31828  leopmuli  32069  mdslmd1lem2  32262  chirredlem2  32327  chirredi  32330  cdjreui  32368  addltmulALT  32382  reofld  33322  xrge0iifcnv  33930  funtransport  36026  btwnconn1lem13  36094  btwnconn1lem14  36095  outsideofeu  36126  outsidele  36127  funray  36135  lineintmo  36152  bj-nnfan  36743  bj-nnfor  36745  icoreclin  37352  poimirlem27  37648  heicant  37656  itg2gt0cn  37676  bndss  37787  isdrngo3  37960  riscer  37989  intidl  38030  rimco  42513  unxpwdom3  43091  gbegt5  47766