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  2407  nfeqf  2413  frminex  5640  trin2  6123  funprg  6590  funcnvqp  6600  fnun  6649  2elresin  6656  f1cof1  6786  f1oun  6840  f1oco  6844  fvreseq0  7033  f1mpt  7259  poxp  8120  soxp  8121  poseq  8150  wfr3g  8312  tfrlem7  8366  oeoe  8581  brecop  8804  pmss12g  8863  dif1ennnALT  9233  fiin  9378  tcmin  9704  frr3g  9724  harval2  9979  genpv  10979  genpdm  10982  genpnnp  10985  genpcd  10986  genpnmax  10987  addcmpblnr  11049  ltsrpr  11057  addclsr  11063  mulclsr  11064  addasssr  11068  mulasssr  11070  distrsr  11071  mulgt0sr  11085  addresr  11118  mulresr  11119  axaddf  11125  axmulf  11126  axaddass  11136  axmulass  11137  axdistr  11138  mulgt0  11282  mul4  11373  add4  11426  2addsub  11466  addsubeq4  11467  sub4  11498  muladd  11641  mulsub  11652  mulge0  11727  add20i  11752  mulge0i  11756  mulne0  11851  divmuldiv  11910  rec11i  11951  ltmul12a  12066  mulge0b  12080  zmulcl  12638  uz2mulcl  12945  qaddcl  12984  qmulcl  12986  qreccl  12988  rpaddcl  13035  xmulgt0  13304  xmulge0  13305  ixxin  13384  ge0addcl  13482  ge0xaddcl  13484  fzadd2  13583  serge0  14088  expge1  14131  sqrmo  15298  rexanuz  15393  amgm2  15417  bhmafibid1cn  15513  bhmafibid2cn  15514  mulcn2  15643  dvds2ln  16342  opoe  16416  omoe  16417  opeo  16418  omeo  16419  divalglem6  16451  divalglem8  16453  lcmcllem  16649  lcmgcd  16660  lcmdvds  16661  pc2dvds  16934  catpropd  17760  gimco  19333  efgrelexlemb  19815  rimco  20595  isdrng5  20854  psgnghm  21730  pf1ind  22515  tgcl  23126  innei  23282  iunconnlem  23584  txbas  23724  txss12  23762  txbasval  23763  tx1stc  23807  fbunfip  24026  tsmsxp  24312  blsscls2  24661  bddnghm  24883  qtopbaslem  24915  iimulcl  25096  icoopnst  25098  iocopnst  25099  iccpnfcnv  25103  mumullem2  27344  fsumvma  27377  lgslem3  27463  pntrsumbnd2  27731  mulsuniflem  28342  readdscl  28692  remulscllem2  28694  remulscl  28695  ajmoi  31210  hvadd4  31388  hvsub4  31389  shsel3  31667  shscli  31669  shscom  31671  chj4  31887  5oalem3  32008  5oalem5  32010  5oalem6  32011  hoadd4  32136  adjmo  32184  adjsym  32185  cnvadj  32244  leopmuli  32485  mdslmd1lem2  32678  chirredlem2  32743  chirredi  32746  cdjreui  32784  addltmulALT  32798  reofld  33663  xrge0iifcnv  34323  funtransport  36523  btwnconn1lem13  36591  btwnconn1lem14  36592  outsideofeu  36623  outsidele  36624  funray  36632  lineintmo  36649  nmuladdss  36690  bj-nnfan  37379  bj-nnfor  37381  icoreclin  38003  poimirlem27  38298  heicant  38306  itg2gt0cn  38326  bndss  38437  isdrngo3  38610  riscer  38639  intidl  38680  unxpwdom3  43822  gbegt5  48526