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  2404  nfeqf  2410  frminex  5630  trin2  6119  funprg  6599  funcnvqp  6609  fnun  6658  2elresin  6665  f1cof1  6795  f1oun  6849  f1oco  6853  fvreseq0  7042  f1mpt  7269  poxp  8147  soxp  8148  poseq  8182  wfr3g  8345  tfrlem7  8399  oeoe  8616  brecop  8839  pmss12g  8905  dif1ennnALT  9276  fiin  9421  tcmin  9747  frr3g  9767  harval2  10085  genpv  11091  genpdm  11094  genpnnp  11097  genpcd  11098  genpnmax  11099  addcmpblnr  11161  ltsrpr  11169  addclsr  11175  mulclsr  11176  addasssr  11180  mulasssr  11182  distrsr  11183  mulgt0sr  11197  addresr  11230  mulresr  11231  axaddf  11237  axmulf  11238  axaddass  11248  axmulass  11249  axdistr  11250  mulgt0  11394  mul4  11485  add4  11538  2addsub  11578  addsubeq4  11579  sub4  11610  muladd  11755  mulsub  11766  mulge0  11841  add20i  11866  mulge0i  11870  mulne0  11965  divmuldiv  12024  rec11i  12065  ltmul12a  12180  mulge0b  12194  zmulcl  12752  uz2mulcl  13060  qaddcl  13100  qmulcl  13102  qreccl  13104  rpaddcl  13151  xmulgt0  13420  xmulge0  13421  ixxin  13500  ge0addcl  13598  ge0xaddcl  13600  fzadd2  13700  serge0  14206  expge1  14249  sqrmo  15427  rexanuz  15522  amgm2  15546  bhmafibid1cn  15642  bhmafibid2cn  15643  mulcn2  15772  dvds2ln  16468  opoe  16542  omoe  16543  opeo  16544  omeo  16545  divalglem6  16577  divalglem8  16579  lcmcllem  16780  lcmgcd  16791  lcmdvds  16792  pc2dvds  17066  catpropd  17892  gimco  19491  efgrelexlemb  19973  rimco  20756  isdrng5  21017  psgnghm  21895  pf1ind  22682  tgcl  23296  innei  23452  iunconnlem  23754  txbas  23895  txss12  23933  txbasval  23934  tx1stc  23978  fbunfip  24197  tsmsxp  24483  blsscls2  24832  bddnghm  25054  qtopbaslem  25086  iimulcl  25267  icoopnst  25269  iocopnst  25270  iccpnfcnv  25274  mumullem2  27516  fsumvma  27549  lgslem3  27635  pntrsumbnd2  27903  mulsuniflem  28544  readdscl  28894  remulscllem2  28896  remulscl  28897  ajmoi  31469  hvadd4  31647  hvsub4  31648  shsel3  31926  shscli  31928  shscom  31930  chj4  32146  5oalem3  32267  5oalem5  32269  5oalem6  32270  hoadd4  32395  adjmo  32443  adjsym  32444  cnvadj  32503  leopmuli  32744  mdslmd1lem2  32937  chirredlem2  33002  chirredi  33005  cdjreui  33043  addltmulALT  33099  reofld  33954  xrge0iifcnv  34615  dfac16  35822  funtransport  36920  btwnconn1lem13  36988  btwnconn1lem14  36989  outsideofeu  37020  outsidele  37021  funray  37029  lineintmo  37046  nmuladdss  37086  bj-nnfan  37780  bj-nnfor  37782  icoreclin  38417  poimirlem27  38702  heicant  38710  itg2gt0cn  38730  bndss  38857  isdrngo3  39030  riscer  39059  intidl  39100  unxpwdom3  44234  gbegt5  48995