Theorem an4s 656

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 652	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 216	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 206  df-an 396

This theorem is referenced by:  an42s  657  anandis  674  anandirs  675  ax13  2375  nfeqf  2381  frminex  5560  trin2  6017  funprg  6472  funcnvqp  6482  fnun  6529  2elresin  6537  f1cof1  6665  f1coOLD  6667  f1oun  6719  f1oco  6722  fvreseq0  6897  f1mpt  7115  poxp  7940  soxp  7941  wfr3g  8109  wfrfunOLD  8121  tfrlem7  8185  oeoe  8392  brecop  8557  pmss12g  8615  dif1enALT  8980  fiin  9111  tcmin  9430  frr3g  9445  harval2  9686  genpv  10686  genpdm  10689  genpnnp  10692  genpcd  10693  genpnmax  10694  addcmpblnr  10756  ltsrpr  10764  addclsr  10770  mulclsr  10771  addasssr  10775  mulasssr  10777  distrsr  10778  mulgt0sr  10792  addresr  10825  mulresr  10826  axaddf  10832  axmulf  10833  axaddass  10843  axmulass  10844  axdistr  10845  mulgt0  10983  mul4  11073  add4  11125  2addsub  11165  addsubeq4  11166  sub4  11196  muladd  11337  mulsub  11348  mulge0  11423  add20i  11448  mulge0i  11452  mulne0  11547  divmuldiv  11605  rec11i  11646  ltmul12a  11761  mulge0b  11775  zmulcl  12299  uz2mulcl  12595  qaddcl  12634  qmulcl  12636  qreccl  12638  rpaddcl  12681  xmulgt0  12946  xmulge0  12947  ixxin  13025  ge0addcl  13121  ge0xaddcl  13123  fzadd2  13220  serge0  13705  expge1  13748  sqrmo  14891  rexanuz  14985  amgm2  15009  bhmafibid1cn  15103  bhmafibid2cn  15104  mulcn2  15233  dvds2ln  15926  opoe  16000  omoe  16001  opeo  16002  omeo  16003  divalglem6  16035  divalglem8  16037  lcmcllem  16229  lcmgcd  16240  lcmdvds  16241  pc2dvds  16508  catpropd  17335  gimco  18799  efgrelexlemb  19271  psgnghm  20697  pf1ind  21431  tgcl  22027  innei  22184  iunconnlem  22486  txbas  22626  txss12  22664  txbasval  22665  tx1stc  22709  fbunfip  22928  tsmsxp  23214  blsscls2  23566  bddnghm  23796  qtopbaslem  23828  iimulcl  24006  icoopnst  24008  iocopnst  24009  iccpnfcnv  24013  mumullem2  26234  fsumvma  26266  lgslem3  26352  pntrsumbnd2  26620  ajmoi  29121  hvadd4  29299  hvsub4  29300  shsel3  29578  shscli  29580  shscom  29582  chj4  29798  5oalem3  29919  5oalem5  29921  5oalem6  29922  hoadd4  30047  adjmo  30095  adjsym  30096  cnvadj  30155  leopmuli  30396  mdslmd1lem2  30589  chirredlem2  30654  chirredi  30657  cdjreui  30695  addltmulALT  30709  reofld  31446  xrge0iifcnv  31785  poseq  33729  funtransport  34260  btwnconn1lem13  34328  btwnconn1lem14  34329  outsideofeu  34360  outsidele  34361  funray  34369  lineintmo  34386  bj-nnfan  34857  bj-nnfor  34859  icoreclin  35455  poimirlem27  35731  heicant  35739  itg2gt0cn  35759  bndss  35871  isdrngo3  36044  riscer  36073  intidl  36114  unxpwdom3  40836  gbegt5  45101