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  2380  nfeqf  2386  frminex  5664  trin2  6143  funprg  6620  funcnvqp  6630  fnun  6682  2elresin  6689  f1cof1  6814  f1oun  6867  f1oco  6871  fvreseq0  7058  f1mpt  7281  poxp  8153  soxp  8154  poseq  8183  wfr3g  8347  wfrfunOLD  8359  tfrlem7  8423  oeoe  8637  brecop  8850  pmss12g  8909  dif1ennnALT  9311  fiin  9462  tcmin  9781  frr3g  9796  harval2  10037  genpv  11039  genpdm  11042  genpnnp  11045  genpcd  11046  genpnmax  11047  addcmpblnr  11109  ltsrpr  11117  addclsr  11123  mulclsr  11124  addasssr  11128  mulasssr  11130  distrsr  11131  mulgt0sr  11145  addresr  11178  mulresr  11179  axaddf  11185  axmulf  11186  axaddass  11196  axmulass  11197  axdistr  11198  mulgt0  11338  mul4  11429  add4  11482  2addsub  11522  addsubeq4  11523  sub4  11554  muladd  11695  mulsub  11706  mulge0  11781  add20i  11806  mulge0i  11810  mulne0  11905  divmuldiv  11967  rec11i  12008  ltmul12a  12123  mulge0b  12138  zmulcl  12666  uz2mulcl  12968  qaddcl  13007  qmulcl  13009  qreccl  13011  rpaddcl  13057  xmulgt0  13325  xmulge0  13326  ixxin  13404  ge0addcl  13500  ge0xaddcl  13502  fzadd2  13599  serge0  14097  expge1  14140  sqrmo  15290  rexanuz  15384  amgm2  15408  bhmafibid1cn  15502  bhmafibid2cn  15503  mulcn2  15632  dvds2ln  16326  opoe  16400  omoe  16401  opeo  16402  omeo  16403  divalglem6  16435  divalglem8  16437  lcmcllem  16633  lcmgcd  16644  lcmdvds  16645  pc2dvds  16917  catpropd  17752  gimco  19286  efgrelexlemb  19768  psgnghm  21598  pf1ind  22359  tgcl  22976  innei  23133  iunconnlem  23435  txbas  23575  txss12  23613  txbasval  23614  tx1stc  23658  fbunfip  23877  tsmsxp  24163  blsscls2  24517  bddnghm  24747  qtopbaslem  24779  iimulcl  24966  icoopnst  24969  iocopnst  24970  iccpnfcnv  24975  mumullem2  27223  fsumvma  27257  lgslem3  27343  pntrsumbnd2  27611  mulsuniflem  28175  readdscl  28431  remulscllem2  28433  remulscl  28434  ajmoi  30877  hvadd4  31055  hvsub4  31056  shsel3  31334  shscli  31336  shscom  31338  chj4  31554  5oalem3  31675  5oalem5  31677  5oalem6  31678  hoadd4  31803  adjmo  31851  adjsym  31852  cnvadj  31911  leopmuli  32152  mdslmd1lem2  32345  chirredlem2  32410  chirredi  32413  cdjreui  32451  addltmulALT  32465  reofld  33372  xrge0iifcnv  33932  funtransport  36032  btwnconn1lem13  36100  btwnconn1lem14  36101  outsideofeu  36132  outsidele  36133  funray  36141  lineintmo  36158  bj-nnfan  36749  bj-nnfor  36751  icoreclin  37358  poimirlem27  37654  heicant  37662  itg2gt0cn  37682  bndss  37793  isdrngo3  37966  riscer  37995  intidl  38036  rimco  42528  unxpwdom3  43107  gbegt5  47748