Theorem an4s 656

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  an42s  657  anandis  674  anandirs  675  ax13  2349  nfeqf  2356  frminex  5430  trin2  5866  funprg  6285  funcnvqp  6295  fnun  6340  2elresin  6345  f1co  6460  f1oun  6509  f1oco  6512  fvreseq0  6680  f1mpt  6891  poxp  7682  soxp  7683  wfr3g  7811  wfrfun  7824  tfrlem7  7878  oeoe  8082  brecop  8247  pmss12g  8290  dif1en  8604  fiin  8739  tcmin  9036  harval2  9279  genpv  10274  genpdm  10277  genpnnp  10280  genpcd  10281  genpnmax  10282  addcmpblnr  10344  ltsrpr  10352  addclsr  10358  mulclsr  10359  addasssr  10363  mulasssr  10365  distrsr  10366  mulgt0sr  10380  addresr  10413  mulresr  10414  axaddf  10420  axmulf  10421  axaddass  10431  axmulass  10432  axdistr  10433  mulgt0  10571  mul4  10661  add4  10713  2addsub  10754  addsubeq4  10755  sub4  10785  muladd  10926  mulsub  10937  mulge0  11012  add20i  11037  mulge0i  11041  mulne0  11136  divmuldiv  11194  rec11i  11235  ltmul12a  11350  mulge0b  11364  zmulcl  11885  uz2mulcl  12179  qaddcl  12218  qmulcl  12220  qreccl  12222  rpaddcl  12265  xmulgt0  12530  xmulge0  12531  ixxin  12609  ge0addcl  12702  ge0xaddcl  12704  fzadd2  12796  serge0  13278  expge1  13320  sqrmo  14449  rexanuz  14543  amgm2  14567  bhmafibid1cn  14661  bhmafibid2cn  14662  mulcn2  14790  dvds2ln  15479  opoe  15549  omoe  15550  opeo  15551  omeo  15552  divalglem6  15586  divalglem8  15588  lcmcllem  15773  lcmgcd  15784  lcmdvds  15785  pc2dvds  16048  catpropd  16812  gimco  18153  efgrelexlemb  18607  pf1ind  20204  psgnghm  20410  tgcl  21265  innei  21421  iunconnlem  21723  txbas  21863  txss12  21901  txbasval  21902  tx1stc  21946  fbunfip  22165  tsmsxp  22450  blsscls2  22801  bddnghm  23022  qtopbaslem  23054  iimulcl  23228  icoopnst  23230  iocopnst  23231  iccpnfcnv  23235  mumullem2  25443  fsumvma  25475  lgslem3  25561  pntrsumbnd2  25829  ajmoi  28322  hvadd4  28500  hvsub4  28501  shsel3  28779  shscli  28781  shscom  28783  chj4  28999  5oalem3  29120  5oalem5  29122  5oalem6  29123  hoadd4  29248  adjmo  29296  adjsym  29297  cnvadj  29356  leopmuli  29597  mdslmd1lem2  29790  chirredlem2  29855  chirredi  29858  cdjreui  29896  addltmulALT  29910  reofld  30563  xrge0iifcnv  30789  poseq  32706  frr3g  32732  funtransport  33103  btwnconn1lem13  33171  btwnconn1lem14  33172  outsideofeu  33203  outsidele  33204  funray  33212  lineintmo  33229  bj-nnfan  33873  bj-nnfor  33875  icoreclin  34190  poimirlem27  34471  heicant  34479  itg2gt0cn  34499  bndss  34617  isdrngo3  34790  riscer  34819  intidl  34860  unxpwdom3  39201  gbegt5  43430