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  2373  nfeqf  2379  frminex  5598  trin2  6072  funprg  6536  funcnvqp  6546  fnun  6596  2elresin  6603  f1cof1  6730  f1oun  6783  f1oco  6787  fvreseq0  6972  f1mpt  7198  poxp  8061  soxp  8062  poseq  8091  wfr3g  8252  tfrlem7  8305  oeoe  8517  brecop  8737  pmss12g  8796  dif1ennnALT  9166  fiin  9312  tcmin  9637  frr3g  9652  harval2  9893  genpv  10893  genpdm  10896  genpnnp  10899  genpcd  10900  genpnmax  10901  addcmpblnr  10963  ltsrpr  10971  addclsr  10977  mulclsr  10978  addasssr  10982  mulasssr  10984  distrsr  10985  mulgt0sr  10999  addresr  11032  mulresr  11033  axaddf  11039  axmulf  11040  axaddass  11050  axmulass  11051  axdistr  11052  mulgt0  11193  mul4  11284  add4  11337  2addsub  11377  addsubeq4  11378  sub4  11409  muladd  11552  mulsub  11563  mulge0  11638  add20i  11663  mulge0i  11667  mulne0  11762  divmuldiv  11824  rec11i  11865  ltmul12a  11980  mulge0b  11995  zmulcl  12524  uz2mulcl  12827  qaddcl  12866  qmulcl  12868  qreccl  12870  rpaddcl  12917  xmulgt0  13185  xmulge0  13186  ixxin  13265  ge0addcl  13363  ge0xaddcl  13365  fzadd2  13462  serge0  13963  expge1  14006  sqrmo  15158  rexanuz  15253  amgm2  15277  bhmafibid1cn  15373  bhmafibid2cn  15374  mulcn2  15503  dvds2ln  16200  opoe  16274  omoe  16275  opeo  16276  omeo  16277  divalglem6  16309  divalglem8  16311  lcmcllem  16507  lcmgcd  16518  lcmdvds  16519  pc2dvds  16791  catpropd  17615  gimco  19147  efgrelexlemb  19629  psgnghm  21487  pf1ind  22240  tgcl  22854  innei  23010  iunconnlem  23312  txbas  23452  txss12  23490  txbasval  23491  tx1stc  23535  fbunfip  23754  tsmsxp  24040  blsscls2  24390  bddnghm  24612  qtopbaslem  24644  iimulcl  24831  icoopnst  24834  iocopnst  24835  iccpnfcnv  24840  mumullem2  27088  fsumvma  27122  lgslem3  27208  pntrsumbnd2  27476  mulsuniflem  28057  readdscl  28368  remulscllem2  28370  remulscl  28371  ajmoi  30802  hvadd4  30980  hvsub4  30981  shsel3  31259  shscli  31261  shscom  31263  chj4  31479  5oalem3  31600  5oalem5  31602  5oalem6  31603  hoadd4  31728  adjmo  31776  adjsym  31777  cnvadj  31836  leopmuli  32077  mdslmd1lem2  32270  chirredlem2  32335  chirredi  32338  cdjreui  32376  addltmulALT  32390  reofld  33281  xrge0iifcnv  33900  funtransport  36009  btwnconn1lem13  36077  btwnconn1lem14  36078  outsideofeu  36109  outsidele  36110  funray  36118  lineintmo  36135  bj-nnfan  36726  bj-nnfor  36728  icoreclin  37335  poimirlem27  37631  heicant  37639  itg2gt0cn  37659  bndss  37770  isdrngo3  37943  riscer  37972  intidl  38013  rimco  42495  unxpwdom3  43072  gbegt5  47749