Theorem an4s 673

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an42s  674  anandis  691  anandirs  692  ax13  2404  nfeqf  2410  frminex  5634  trin2  6117  funprg  6588  funcnvqp  6598  fnun  6647  2elresin  6654  f1cof1  6784  f1oun  6838  f1oco  6842  fvreseq0  7031  f1mpt  7259  poxp  8127  soxp  8128  poseq  8157  wfr3g  8319  tfrlem7  8373  oeoe  8588  brecop  8811  pmss12g  8877  dif1ennnALT  9248  fiin  9393  tcmin  9719  frr3g  9739  harval2  10003  genpv  11009  genpdm  11012  genpnnp  11015  genpcd  11016  genpnmax  11017  addcmpblnr  11079  ltsrpr  11087  addclsr  11093  mulclsr  11094  addasssr  11098  mulasssr  11100  distrsr  11101  mulgt0sr  11115  addresr  11148  mulresr  11149  axaddf  11155  axmulf  11156  axaddass  11166  axmulass  11167  axdistr  11168  mulgt0  11312  mul4  11403  add4  11456  2addsub  11496  addsubeq4  11497  sub4  11528  muladd  11671  mulsub  11682  mulge0  11757  add20i  11782  mulge0i  11786  mulne0  11881  divmuldiv  11940  rec11i  11981  ltmul12a  12096  mulge0b  12110  zmulcl  12668  uz2mulcl  12976  qaddcl  13016  qmulcl  13018  qreccl  13020  rpaddcl  13067  xmulgt0  13336  xmulge0  13337  ixxin  13416  ge0addcl  13514  ge0xaddcl  13516  fzadd2  13615  serge0  14121  expge1  14164  sqrmo  15339  rexanuz  15434  amgm2  15458  bhmafibid1cn  15554  bhmafibid2cn  15555  mulcn2  15684  dvds2ln  16380  opoe  16454  omoe  16455  opeo  16456  omeo  16457  divalglem6  16489  divalglem8  16491  lcmcllem  16687  lcmgcd  16698  lcmdvds  16699  pc2dvds  16972  catpropd  17798  gimco  19396  efgrelexlemb  19878  rimco  20659  isdrng5  20918  psgnghm  21794  pf1ind  22581  tgcl  23195  innei  23351  iunconnlem  23653  txbas  23794  txss12  23832  txbasval  23833  tx1stc  23877  fbunfip  24096  tsmsxp  24382  blsscls2  24731  bddnghm  24953  qtopbaslem  24985  iimulcl  25166  icoopnst  25168  iocopnst  25169  iccpnfcnv  25173  mumullem2  27417  fsumvma  27450  lgslem3  27536  pntrsumbnd2  27804  mulsuniflem  28415  readdscl  28765  remulscllem2  28767  remulscl  28768  ajmoi  31340  hvadd4  31518  hvsub4  31519  shsel3  31797  shscli  31799  shscom  31801  chj4  32017  5oalem3  32138  5oalem5  32140  5oalem6  32141  hoadd4  32266  adjmo  32314  adjsym  32315  cnvadj  32374  leopmuli  32615  mdslmd1lem2  32808  chirredlem2  32873  chirredi  32876  cdjreui  32914  addltmulALT  32928  reofld  33784  xrge0iifcnv  34444  funtransport  36612  btwnconn1lem13  36680  btwnconn1lem14  36681  outsideofeu  36712  outsidele  36713  funray  36721  lineintmo  36738  nmuladdss  36794  bj-nnfan  37488  bj-nnfor  37490  icoreclin  38112  poimirlem27  38397  heicant  38405  itg2gt0cn  38425  bndss  38537  isdrngo3  38710  riscer  38739  intidl  38780  unxpwdom3  43937  gbegt5  48678