Theorem an4s 660

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 656	. 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  661  anandis  678  anandirs  679  ax13  2379  nfeqf  2385  frminex  5633  trin2  6112  funprg  6589  funcnvqp  6599  fnun  6651  2elresin  6658  f1cof1  6783  f1oun  6836  f1oco  6840  fvreseq0  7027  f1mpt  7253  poxp  8125  soxp  8126  poseq  8155  wfr3g  8319  wfrfunOLD  8331  tfrlem7  8395  oeoe  8609  brecop  8822  pmss12g  8881  dif1ennnALT  9281  fiin  9432  tcmin  9753  frr3g  9768  harval2  10009  genpv  11011  genpdm  11014  genpnnp  11017  genpcd  11018  genpnmax  11019  addcmpblnr  11081  ltsrpr  11089  addclsr  11095  mulclsr  11096  addasssr  11100  mulasssr  11102  distrsr  11103  mulgt0sr  11117  addresr  11150  mulresr  11151  axaddf  11157  axmulf  11158  axaddass  11168  axmulass  11169  axdistr  11170  mulgt0  11310  mul4  11401  add4  11454  2addsub  11494  addsubeq4  11495  sub4  11526  muladd  11667  mulsub  11678  mulge0  11753  add20i  11778  mulge0i  11782  mulne0  11877  divmuldiv  11939  rec11i  11980  ltmul12a  12095  mulge0b  12110  zmulcl  12639  uz2mulcl  12940  qaddcl  12979  qmulcl  12981  qreccl  12983  rpaddcl  13029  xmulgt0  13297  xmulge0  13298  ixxin  13377  ge0addcl  13475  ge0xaddcl  13477  fzadd2  13574  serge0  14072  expge1  14115  sqrmo  15268  rexanuz  15362  amgm2  15386  bhmafibid1cn  15480  bhmafibid2cn  15481  mulcn2  15610  dvds2ln  16306  opoe  16380  omoe  16381  opeo  16382  omeo  16383  divalglem6  16415  divalglem8  16417  lcmcllem  16613  lcmgcd  16624  lcmdvds  16625  pc2dvds  16897  catpropd  17719  gimco  19249  efgrelexlemb  19729  psgnghm  21538  pf1ind  22291  tgcl  22905  innei  23061  iunconnlem  23363  txbas  23503  txss12  23541  txbasval  23542  tx1stc  23586  fbunfip  23805  tsmsxp  24091  blsscls2  24441  bddnghm  24663  qtopbaslem  24695  iimulcl  24882  icoopnst  24885  iocopnst  24886  iccpnfcnv  24891  mumullem2  27140  fsumvma  27174  lgslem3  27260  pntrsumbnd2  27528  mulsuniflem  28092  readdscl  28348  remulscllem2  28350  remulscl  28351  ajmoi  30785  hvadd4  30963  hvsub4  30964  shsel3  31242  shscli  31244  shscom  31246  chj4  31462  5oalem3  31583  5oalem5  31585  5oalem6  31586  hoadd4  31711  adjmo  31759  adjsym  31760  cnvadj  31819  leopmuli  32060  mdslmd1lem2  32253  chirredlem2  32318  chirredi  32321  cdjreui  32359  addltmulALT  32373  reofld  33305  xrge0iifcnv  33910  funtransport  35995  btwnconn1lem13  36063  btwnconn1lem14  36064  outsideofeu  36095  outsidele  36096  funray  36104  lineintmo  36121  bj-nnfan  36712  bj-nnfor  36714  icoreclin  37321  poimirlem27  37617  heicant  37625  itg2gt0cn  37645  bndss  37756  isdrngo3  37929  riscer  37958  intidl  37999  rimco  42488  unxpwdom3  43066  gbegt5  47723