Theorem an4s 659

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  an42s  660  anandis  677  anandirs  678  ax13  2375  nfeqf  2381  frminex  5657  trin2  6125  funprg  6603  funcnvqp  6613  fnun  6664  2elresin  6672  f1cof1  6799  f1coOLD  6801  f1oun  6853  f1oco  6857  fvreseq0  7040  f1mpt  7260  poxp  8114  soxp  8115  poseq  8144  wfr3g  8307  wfrfunOLD  8319  tfrlem7  8383  oeoe  8599  brecop  8804  pmss12g  8863  dif1ennnALT  9277  fiin  9417  tcmin  9736  frr3g  9751  harval2  9992  genpv  10994  genpdm  10997  genpnnp  11000  genpcd  11001  genpnmax  11002  addcmpblnr  11064  ltsrpr  11072  addclsr  11078  mulclsr  11079  addasssr  11083  mulasssr  11085  distrsr  11086  mulgt0sr  11100  addresr  11133  mulresr  11134  axaddf  11140  axmulf  11141  axaddass  11151  axmulass  11152  axdistr  11153  mulgt0  11291  mul4  11382  add4  11434  2addsub  11474  addsubeq4  11475  sub4  11505  muladd  11646  mulsub  11657  mulge0  11732  add20i  11757  mulge0i  11761  mulne0  11856  divmuldiv  11914  rec11i  11955  ltmul12a  12070  mulge0b  12084  zmulcl  12611  uz2mulcl  12910  qaddcl  12949  qmulcl  12951  qreccl  12953  rpaddcl  12996  xmulgt0  13262  xmulge0  13263  ixxin  13341  ge0addcl  13437  ge0xaddcl  13439  fzadd2  13536  serge0  14022  expge1  14065  sqrmo  15198  rexanuz  15292  amgm2  15316  bhmafibid1cn  15410  bhmafibid2cn  15411  mulcn2  15540  dvds2ln  16232  opoe  16306  omoe  16307  opeo  16308  omeo  16309  divalglem6  16341  divalglem8  16343  lcmcllem  16533  lcmgcd  16544  lcmdvds  16545  pc2dvds  16812  catpropd  17653  gimco  19142  efgrelexlemb  19618  psgnghm  21133  pf1ind  21874  tgcl  22472  innei  22629  iunconnlem  22931  txbas  23071  txss12  23109  txbasval  23110  tx1stc  23154  fbunfip  23373  tsmsxp  23659  blsscls2  24013  bddnghm  24243  qtopbaslem  24275  iimulcl  24453  icoopnst  24455  iocopnst  24456  iccpnfcnv  24460  mumullem2  26684  fsumvma  26716  lgslem3  26802  pntrsumbnd2  27070  mulsuniflem  27604  ajmoi  30111  hvadd4  30289  hvsub4  30290  shsel3  30568  shscli  30570  shscom  30572  chj4  30788  5oalem3  30909  5oalem5  30911  5oalem6  30912  hoadd4  31037  adjmo  31085  adjsym  31086  cnvadj  31145  leopmuli  31386  mdslmd1lem2  31579  chirredlem2  31644  chirredi  31647  cdjreui  31685  addltmulALT  31699  reofld  32459  xrge0iifcnv  32913  funtransport  35003  btwnconn1lem13  35071  btwnconn1lem14  35072  outsideofeu  35103  outsidele  35104  funray  35112  lineintmo  35129  bj-nnfan  35626  bj-nnfor  35628  icoreclin  36238  poimirlem27  36515  heicant  36523  itg2gt0cn  36543  bndss  36654  isdrngo3  36827  riscer  36856  intidl  36897  rimco  41093  unxpwdom3  41837  gbegt5  46429