Theorem an4s 672

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  an42s  673  anandis  690  anandirs  691  ax13  2413  nfeqf  2419  frminex  5641  trin2  6124  funprg  6591  funcnvqp  6601  fnun  6650  2elresin  6657  f1cof1  6787  f1oun  6841  f1oco  6845  fvreseq0  7034  f1mpt  7260  poxp  8123  soxp  8124  poseq  8153  wfr3g  8315  tfrlem7  8369  oeoe  8584  brecop  8807  pmss12g  8866  dif1ennnALT  9236  fiin  9381  tcmin  9707  frr3g  9727  harval2  9982  genpv  10983  genpdm  10986  genpnnp  10989  genpcd  10990  genpnmax  10991  addcmpblnr  11053  ltsrpr  11061  addclsr  11067  mulclsr  11068  addasssr  11072  mulasssr  11074  distrsr  11075  mulgt0sr  11089  addresr  11122  mulresr  11123  axaddf  11129  axmulf  11130  axaddass  11140  axmulass  11141  axdistr  11142  mulgt0  11286  mul4  11377  add4  11430  2addsub  11470  addsubeq4  11471  sub4  11502  muladd  11645  mulsub  11656  mulge0  11731  add20i  11756  mulge0i  11760  mulne0  11855  divmuldiv  11914  rec11i  11955  ltmul12a  12070  mulge0b  12084  zmulcl  12642  uz2mulcl  12949  qaddcl  12988  qmulcl  12990  qreccl  12992  rpaddcl  13039  xmulgt0  13308  xmulge0  13309  ixxin  13388  ge0addcl  13486  ge0xaddcl  13488  fzadd2  13586  serge0  14091  expge1  14134  sqrmo  15301  rexanuz  15396  amgm2  15420  bhmafibid1cn  15516  bhmafibid2cn  15517  mulcn2  15646  dvds2ln  16346  opoe  16420  omoe  16421  opeo  16422  omeo  16423  divalglem6  16455  divalglem8  16457  lcmcllem  16653  lcmgcd  16664  lcmdvds  16665  pc2dvds  16938  catpropd  17764  gimco  19337  efgrelexlemb  19819  psgnghm  21698  pf1ind  22483  tgcl  23094  innei  23250  iunconnlem  23552  txbas  23692  txss12  23730  txbasval  23731  tx1stc  23775  fbunfip  23994  tsmsxp  24280  blsscls2  24629  bddnghm  24851  qtopbaslem  24883  iimulcl  25064  icoopnst  25066  iocopnst  25067  iccpnfcnv  25071  mumullem2  27309  fsumvma  27342  lgslem3  27428  pntrsumbnd2  27696  mulsuniflem  28307  readdscl  28657  remulscllem2  28659  remulscl  28660  ajmoi  31150  hvadd4  31328  hvsub4  31329  shsel3  31607  shscli  31609  shscom  31611  chj4  31827  5oalem3  31948  5oalem5  31950  5oalem6  31951  hoadd4  32076  adjmo  32124  adjsym  32125  cnvadj  32184  leopmuli  32425  mdslmd1lem2  32618  chirredlem2  32683  chirredi  32686  cdjreui  32724  addltmulALT  32738  reofld  33605  xrge0iifcnv  34267  funtransport  36421  btwnconn1lem13  36489  btwnconn1lem14  36490  outsideofeu  36521  outsidele  36522  funray  36530  lineintmo  36547  bj-nnfan  37267  bj-nnfor  37269  icoreclin  37890  poimirlem27  38185  heicant  38193  itg2gt0cn  38213  bndss  38324  isdrngo3  38497  riscer  38526  intidl  38567  rimco  43178  unxpwdom3  43713  gbegt5  48414