Theorem an4s 868

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 864	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 207	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

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  869  anandis  872  anandirs  873  ax13  2248  nfeqf  2300  frminex  5064  trin2  5488  funprg  5908  funcnvqp  5920  fnun  5965  2elresin  5970  f1co  6077  f1oun  6123  f1oco  6126  fvreseq0  6283  f1mpt  6483  poxp  7249  soxp  7250  wfr3g  7373  wfrfun  7385  tfrlem7  7439  oeoe  7639  brecop  7800  pmss12g  7844  dif1en  8153  fiin  8288  tcmin  8577  harval2  8783  genpv  9781  genpdm  9784  genpnnp  9787  genpcd  9788  genpnmax  9789  addcmpblnr  9850  ltsrpr  9858  addclsr  9864  mulclsr  9865  addasssr  9869  mulasssr  9871  distrsr  9872  mulgt0sr  9886  addresr  9919  mulresr  9920  axaddf  9926  axmulf  9927  axaddass  9937  axmulass  9938  axdistr  9939  mulgt0  10075  mul4  10165  add4  10216  2addsub  10255  addsubeq4  10256  sub4  10286  muladd  10422  mulsub  10433  mulge0  10506  add20i  10531  mulge0i  10535  mulne0  10629  divmuldiv  10685  rec11i  10726  ltmul12a  10839  mulge0b  10853  zmulcl  11386  uz2mulcl  11726  qaddcl  11764  qmulcl  11766  qreccl  11768  rpaddcl  11814  xmulgt0  12072  xmulge0  12073  ixxin  12150  ge0addcl  12242  ge0xaddcl  12244  fzadd2  12334  serge0  12811  expge1  12853  sqrmo  13942  rexanuz  14035  amgm2  14059  mulcn2  14276  dvds2ln  14957  opoe  15030  omoe  15031  opeo  15032  omeo  15033  divalglem6  15064  divalglem8  15066  lcmcllem  15252  lcmgcd  15263  lcmdvds  15264  pc2dvds  15526  catpropd  16309  gimco  17650  efgrelexlemb  18103  pf1ind  19659  psgnghm  19866  tgcl  20713  innei  20869  iunconnlem  21170  txbas  21310  txss12  21348  txbasval  21349  tx1stc  21393  fbunfip  21613  tsmsxp  21898  blsscls2  22249  bddnghm  22470  qtopbaslem  22502  iimulcl  22676  icoopnst  22678  iocopnst  22679  iccpnfcnv  22683  mumullem2  24840  fsumvma  24872  lgslem3  24958  pntrsumbnd2  25190  wlknwwlksnfun  26677  ajmoi  27602  hvadd4  27781  hvsub4  27782  shsel3  28062  shscli  28064  shscom  28066  chj4  28282  5oalem3  28403  5oalem5  28405  5oalem6  28406  hoadd4  28531  adjmo  28579  adjsym  28580  cnvadj  28639  leopmuli  28880  mdslmd1lem2  29073  chirredlem2  29138  chirredi  29141  cdjreui  29179  addltmulALT  29193  reofld  29667  xrge0iifcnv  29803  poseq  31504  frr3g  31533  frrlem4  31537  frrlem5c  31540  funtransport  31833  btwnconn1lem13  31901  btwnconn1lem14  31902  outsideofeu  31933  outsidele  31934  funray  31942  lineintmo  31959  icoreclin  32876  poimirlem27  33107  heicant  33115  itg2gt0cn  33136  bndss  33256  isdrngo3  33429  riscer  33458  intidl  33499  unxpwdom3  37184  gbegt5  40974