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  2379  nfeqf  2385  frminex  5610  trin2  6086  funprg  6552  funcnvqp  6562  fnun  6612  2elresin  6619  f1cof1  6746  f1oun  6799  f1oco  6803  fvreseq0  6990  f1mpt  7216  poxp  8078  soxp  8079  poseq  8108  wfr3g  8269  tfrlem7  8322  oeoe  8535  brecop  8757  pmss12g  8817  dif1ennnALT  9187  fiin  9335  tcmin  9660  frr3g  9680  harval2  9921  genpv  10922  genpdm  10925  genpnnp  10928  genpcd  10929  genpnmax  10930  addcmpblnr  10992  ltsrpr  11000  addclsr  11006  mulclsr  11007  addasssr  11011  mulasssr  11013  distrsr  11014  mulgt0sr  11028  addresr  11061  mulresr  11062  axaddf  11068  axmulf  11069  axaddass  11079  axmulass  11080  axdistr  11081  mulgt0  11223  mul4  11314  add4  11367  2addsub  11407  addsubeq4  11408  sub4  11439  muladd  11582  mulsub  11593  mulge0  11668  add20i  11693  mulge0i  11697  mulne0  11792  divmuldiv  11855  rec11i  11896  ltmul12a  12011  mulge0b  12026  zmulcl  12576  uz2mulcl  12876  qaddcl  12915  qmulcl  12917  qreccl  12919  rpaddcl  12966  xmulgt0  13235  xmulge0  13236  ixxin  13315  ge0addcl  13413  ge0xaddcl  13415  fzadd2  13513  serge0  14018  expge1  14061  sqrmo  15213  rexanuz  15308  amgm2  15332  bhmafibid1cn  15428  bhmafibid2cn  15429  mulcn2  15558  dvds2ln  16258  opoe  16332  omoe  16333  opeo  16334  omeo  16335  divalglem6  16367  divalglem8  16369  lcmcllem  16565  lcmgcd  16576  lcmdvds  16577  pc2dvds  16850  catpropd  17675  gimco  19243  efgrelexlemb  19725  psgnghm  21560  pf1ind  22320  tgcl  22934  innei  23090  iunconnlem  23392  txbas  23532  txss12  23570  txbasval  23571  tx1stc  23615  fbunfip  23834  tsmsxp  24120  blsscls2  24469  bddnghm  24691  qtopbaslem  24723  iimulcl  24904  icoopnst  24906  iocopnst  24907  iccpnfcnv  24911  mumullem2  27143  fsumvma  27176  lgslem3  27262  pntrsumbnd2  27530  mulsuniflem  28141  readdscl  28491  remulscllem2  28493  remulscl  28494  ajmoi  30929  hvadd4  31107  hvsub4  31108  shsel3  31386  shscli  31388  shscom  31390  chj4  31606  5oalem3  31727  5oalem5  31729  5oalem6  31730  hoadd4  31855  adjmo  31903  adjsym  31904  cnvadj  31963  leopmuli  32204  mdslmd1lem2  32397  chirredlem2  32462  chirredi  32465  cdjreui  32503  addltmulALT  32517  reofld  33403  xrge0iifcnv  34077  funtransport  36213  btwnconn1lem13  36281  btwnconn1lem14  36282  outsideofeu  36313  outsidele  36314  funray  36322  lineintmo  36339  bj-nnfan  37051  bj-nnfor  37053  icoreclin  37673  poimirlem27  37968  heicant  37976  itg2gt0cn  37996  bndss  38107  isdrngo3  38280  riscer  38309  intidl  38350  rimco  42963  unxpwdom3  43523  gbegt5  48237