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  2373  nfeqf  2379  frminex  5617  trin2  6096  funprg  6570  funcnvqp  6580  fnun  6632  2elresin  6639  f1cof1  6766  f1oun  6819  f1oco  6823  fvreseq0  7010  f1mpt  7236  poxp  8107  soxp  8108  poseq  8137  wfr3g  8298  tfrlem7  8351  oeoe  8563  brecop  8783  pmss12g  8842  dif1ennnALT  9222  fiin  9373  tcmin  9694  frr3g  9709  harval2  9950  genpv  10952  genpdm  10955  genpnnp  10958  genpcd  10959  genpnmax  10960  addcmpblnr  11022  ltsrpr  11030  addclsr  11036  mulclsr  11037  addasssr  11041  mulasssr  11043  distrsr  11044  mulgt0sr  11058  addresr  11091  mulresr  11092  axaddf  11098  axmulf  11099  axaddass  11109  axmulass  11110  axdistr  11111  mulgt0  11251  mul4  11342  add4  11395  2addsub  11435  addsubeq4  11436  sub4  11467  muladd  11610  mulsub  11621  mulge0  11696  add20i  11721  mulge0i  11725  mulne0  11820  divmuldiv  11882  rec11i  11923  ltmul12a  12038  mulge0b  12053  zmulcl  12582  uz2mulcl  12885  qaddcl  12924  qmulcl  12926  qreccl  12928  rpaddcl  12975  xmulgt0  13243  xmulge0  13244  ixxin  13323  ge0addcl  13421  ge0xaddcl  13423  fzadd2  13520  serge0  14021  expge1  14064  sqrmo  15217  rexanuz  15312  amgm2  15336  bhmafibid1cn  15432  bhmafibid2cn  15433  mulcn2  15562  dvds2ln  16259  opoe  16333  omoe  16334  opeo  16335  omeo  16336  divalglem6  16368  divalglem8  16370  lcmcllem  16566  lcmgcd  16577  lcmdvds  16578  pc2dvds  16850  catpropd  17670  gimco  19200  efgrelexlemb  19680  psgnghm  21489  pf1ind  22242  tgcl  22856  innei  23012  iunconnlem  23314  txbas  23454  txss12  23492  txbasval  23493  tx1stc  23537  fbunfip  23756  tsmsxp  24042  blsscls2  24392  bddnghm  24614  qtopbaslem  24646  iimulcl  24833  icoopnst  24836  iocopnst  24837  iccpnfcnv  24842  mumullem2  27090  fsumvma  27124  lgslem3  27210  pntrsumbnd2  27478  mulsuniflem  28052  readdscl  28350  remulscllem2  28352  remulscl  28353  ajmoi  30787  hvadd4  30965  hvsub4  30966  shsel3  31244  shscli  31246  shscom  31248  chj4  31464  5oalem3  31585  5oalem5  31587  5oalem6  31588  hoadd4  31713  adjmo  31761  adjsym  31762  cnvadj  31821  leopmuli  32062  mdslmd1lem2  32255  chirredlem2  32320  chirredi  32323  cdjreui  32361  addltmulALT  32375  reofld  33315  xrge0iifcnv  33923  funtransport  36019  btwnconn1lem13  36087  btwnconn1lem14  36088  outsideofeu  36119  outsidele  36120  funray  36128  lineintmo  36145  bj-nnfan  36736  bj-nnfor  36738  icoreclin  37345  poimirlem27  37641  heicant  37649  itg2gt0cn  37669  bndss  37780  isdrngo3  37953  riscer  37982  intidl  38023  rimco  42506  unxpwdom3  43084  gbegt5  47762