Theorem an4s 661

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an42s  662  anandis  679  anandirs  680  ax13  2380  nfeqf  2386  frminex  5604  trin2  6081  funprg  6547  funcnvqp  6557  fnun  6607  2elresin  6614  f1cof1  6741  f1oun  6794  f1oco  6798  fvreseq0  6985  f1mpt  7210  poxp  8072  soxp  8073  poseq  8102  wfr3g  8263  tfrlem7  8316  oeoe  8529  brecop  8751  pmss12g  8811  dif1ennnALT  9181  fiin  9329  tcmin  9654  frr3g  9674  harval2  9915  genpv  10916  genpdm  10919  genpnnp  10922  genpcd  10923  genpnmax  10924  addcmpblnr  10986  ltsrpr  10994  addclsr  11000  mulclsr  11001  addasssr  11005  mulasssr  11007  distrsr  11008  mulgt0sr  11022  addresr  11055  mulresr  11056  axaddf  11062  axmulf  11063  axaddass  11073  axmulass  11074  axdistr  11075  mulgt0  11217  mul4  11308  add4  11361  2addsub  11401  addsubeq4  11402  sub4  11433  muladd  11576  mulsub  11587  mulge0  11662  add20i  11687  mulge0i  11691  mulne0  11786  divmuldiv  11849  rec11i  11890  ltmul12a  12005  mulge0b  12020  zmulcl  12570  uz2mulcl  12870  qaddcl  12909  qmulcl  12911  qreccl  12913  rpaddcl  12960  xmulgt0  13229  xmulge0  13230  ixxin  13309  ge0addcl  13407  ge0xaddcl  13409  fzadd2  13507  serge0  14012  expge1  14055  sqrmo  15207  rexanuz  15302  amgm2  15326  bhmafibid1cn  15422  bhmafibid2cn  15423  mulcn2  15552  dvds2ln  16252  opoe  16326  omoe  16327  opeo  16328  omeo  16329  divalglem6  16361  divalglem8  16363  lcmcllem  16559  lcmgcd  16570  lcmdvds  16571  pc2dvds  16844  catpropd  17669  gimco  19237  efgrelexlemb  19719  psgnghm  21573  pf1ind  22333  tgcl  22947  innei  23103  iunconnlem  23405  txbas  23545  txss12  23583  txbasval  23584  tx1stc  23628  fbunfip  23847  tsmsxp  24133  blsscls2  24482  bddnghm  24704  qtopbaslem  24736  iimulcl  24917  icoopnst  24919  iocopnst  24920  iccpnfcnv  24924  mumullem2  27160  fsumvma  27193  lgslem3  27279  pntrsumbnd2  27547  mulsuniflem  28158  readdscl  28508  remulscllem2  28510  remulscl  28511  ajmoi  30947  hvadd4  31125  hvsub4  31126  shsel3  31404  shscli  31406  shscom  31408  chj4  31624  5oalem3  31745  5oalem5  31747  5oalem6  31748  hoadd4  31873  adjmo  31921  adjsym  31922  cnvadj  31981  leopmuli  32222  mdslmd1lem2  32415  chirredlem2  32480  chirredi  32483  cdjreui  32521  addltmulALT  32535  reofld  33421  xrge0iifcnv  34096  funtransport  36232  btwnconn1lem13  36300  btwnconn1lem14  36301  outsideofeu  36332  outsidele  36333  funray  36341  lineintmo  36358  bj-nnfan  37070  bj-nnfor  37072  icoreclin  37690  poimirlem27  37985  heicant  37993  itg2gt0cn  38013  bndss  38124  isdrngo3  38297  riscer  38326  intidl  38367  rimco  42980  unxpwdom3  43544  gbegt5  48252