Theorem an4s 865

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  an42s  866  anandis  869  anandirs  870  ax13  2237  nfeqf  2289  frminex  5018  trin2  5438  funprg  5854  funcnvqp  5866  fnun  5911  2elresin  5916  f1co  6023  f1oun  6069  f1oco  6072  fvreseq0  6225  f1mpt  6419  poxp  7176  soxp  7177  wfr3g  7300  wfrfun  7312  tfrlem7  7366  oeoe  7566  brecop  7727  pmss12g  7770  dif1en  8078  fiin  8211  tcmin  8500  harval2  8706  genpv  9700  genpdm  9703  genpnnp  9706  genpcd  9707  genpnmax  9708  addcmpblnr  9769  ltsrpr  9777  addclsr  9783  mulclsr  9784  addasssr  9788  mulasssr  9790  distrsr  9791  mulgt0sr  9805  addresr  9838  mulresr  9839  axaddf  9845  axmulf  9846  axaddass  9856  axmulass  9857  axdistr  9858  mulgt0  9994  mul4  10084  add4  10135  2addsub  10174  addsubeq4  10175  sub4  10205  muladd  10341  mulsub  10352  mulge0  10425  add20i  10450  mulge0i  10454  mulne0  10548  divmuldiv  10604  rec11i  10645  ltmul12a  10758  mulge0b  10772  zmulcl  11303  uz2mulcl  11642  qaddcl  11680  qmulcl  11682  qreccl  11684  rpaddcl  11730  xmulgt0  11985  xmulge0  11986  ixxin  12063  ge0addcl  12155  ge0xaddcl  12157  fzadd2  12247  serge0  12717  expge1  12759  sqrmo  13840  rexanuz  13933  amgm2  13957  mulcn2  14174  dvds2ln  14852  opoe  14925  omoe  14926  opeo  14927  omeo  14928  divalglem6  14959  divalglem8  14961  lcmcllem  15147  lcmgcd  15158  lcmdvds  15159  pc2dvds  15421  catpropd  16192  gimco  17533  efgrelexlemb  17986  pf1ind  19540  psgnghm  19745  tgcl  20584  innei  20739  iunconlem  21040  txbas  21180  txss12  21218  txbasval  21219  tx1stc  21263  fbunfip  21483  tsmsxp  21768  blsscls2  22119  bddnghm  22340  qtopbaslem  22372  iimulcl  22544  icoopnst  22546  iocopnst  22547  iccpnfcnv  22551  mumullem2  24706  fsumvma  24738  lgslem3  24824  pntrsumbnd2  25056  ajmoi  27098  hvadd4  27277  hvsub4  27278  shsel3  27558  shscli  27560  shscom  27562  chj4  27778  5oalem3  27899  5oalem5  27901  5oalem6  27902  hoadd4  28027  adjmo  28075  adjsym  28076  cnvadj  28135  leopmuli  28376  mdslmd1lem2  28569  chirredlem2  28634  chirredi  28637  cdjreui  28675  addltmulALT  28689  reofld  29171  xrge0iifcnv  29307  poseq  30994  frr3g  31023  frrlem4  31027  frrlem5c  31030  funtransport  31308  btwnconn1lem13  31376  btwnconn1lem14  31377  outsideofeu  31408  outsidele  31409  funray  31417  lineintmo  31434  icoreclin  32381  poimirlem27  32606  heicant  32614  itg2gt0cn  32635  bndss  32755  isdrngo3  32928  riscer  32957  intidl  32998  unxpwdom3  36683  gbegt5  40183  wlknwwlksnfun  41085