Theorem an4s 673

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an42s  674  anandis  691  anandirs  692  ax13  2409  nfeqf  2415  frminex  5642  trin2  6125  funprg  6594  funcnvqp  6604  fnun  6653  2elresin  6660  f1cof1  6790  f1oun  6844  f1oco  6848  fvreseq0  7037  f1mpt  7264  poxp  8130  soxp  8131  poseq  8160  wfr3g  8322  tfrlem7  8376  oeoe  8591  brecop  8814  pmss12g  8873  dif1ennnALT  9244  fiin  9389  tcmin  9715  frr3g  9735  harval2  9999  genpv  10999  genpdm  11002  genpnnp  11005  genpcd  11006  genpnmax  11007  addcmpblnr  11069  ltsrpr  11077  addclsr  11083  mulclsr  11084  addasssr  11088  mulasssr  11090  distrsr  11091  mulgt0sr  11105  addresr  11138  mulresr  11139  axaddf  11145  axmulf  11146  axaddass  11156  axmulass  11157  axdistr  11158  mulgt0  11302  mul4  11393  add4  11446  2addsub  11486  addsubeq4  11487  sub4  11518  muladd  11661  mulsub  11672  mulge0  11747  add20i  11772  mulge0i  11776  mulne0  11871  divmuldiv  11930  rec11i  11971  ltmul12a  12086  mulge0b  12100  zmulcl  12658  uz2mulcl  12966  qaddcl  13005  qmulcl  13007  qreccl  13009  rpaddcl  13056  xmulgt0  13325  xmulge0  13326  ixxin  13405  ge0addcl  13503  ge0xaddcl  13505  fzadd2  13604  serge0  14110  expge1  14153  sqrmo  15326  rexanuz  15421  amgm2  15445  bhmafibid1cn  15541  bhmafibid2cn  15542  mulcn2  15671  dvds2ln  16369  opoe  16443  omoe  16444  opeo  16445  omeo  16446  divalglem6  16478  divalglem8  16480  lcmcllem  16676  lcmgcd  16687  lcmdvds  16688  pc2dvds  16961  catpropd  17787  gimco  19382  efgrelexlemb  19864  rimco  20645  isdrng5  20904  psgnghm  21780  pf1ind  22565  tgcl  23176  innei  23332  iunconnlem  23634  txbas  23775  txss12  23813  txbasval  23814  tx1stc  23858  fbunfip  24077  tsmsxp  24363  blsscls2  24712  bddnghm  24934  qtopbaslem  24966  iimulcl  25147  icoopnst  25149  iocopnst  25150  iccpnfcnv  25154  mumullem2  27395  fsumvma  27428  lgslem3  27514  pntrsumbnd2  27782  mulsuniflem  28393  readdscl  28743  remulscllem2  28745  remulscl  28746  ajmoi  31281  hvadd4  31459  hvsub4  31460  shsel3  31738  shscli  31740  shscom  31742  chj4  31958  5oalem3  32079  5oalem5  32081  5oalem6  32082  hoadd4  32207  adjmo  32255  adjsym  32256  cnvadj  32315  leopmuli  32556  mdslmd1lem2  32749  chirredlem2  32814  chirredi  32817  cdjreui  32855  addltmulALT  32869  reofld  33727  xrge0iifcnv  34387  funtransport  36560  btwnconn1lem13  36628  btwnconn1lem14  36629  outsideofeu  36660  outsidele  36661  funray  36669  lineintmo  36686  nmuladdss  36742  bj-nnfan  37436  bj-nnfor  37438  icoreclin  38060  poimirlem27  38355  heicant  38363  itg2gt0cn  38383  bndss  38495  isdrngo3  38668  riscer  38697  intidl  38738  unxpwdom3  43880  gbegt5  48584