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  2407  nfeqf  2413  frminex  5637  trin2  6135  funprg  6624  funcnvqp  6634  fnun  6683  2elresin  6690  f1cof1  6820  f1oun  6874  f1oco  6878  fvreseq0  7068  f1mpt  7296  poxp  8177  soxp  8178  poseq  8212  wfr3g  8375  tfrlem7  8429  oeoe  8646  brecop  8869  pmss12g  8935  dif1ennnALT  9306  fiin  9451  tcmin  9777  frr3g  9797  harval2  10117  genpv  11123  genpdm  11126  genpnnp  11129  genpcd  11130  genpnmax  11131  addcmpblnr  11193  ltsrpr  11201  addclsr  11207  mulclsr  11208  addasssr  11212  mulasssr  11214  distrsr  11215  mulgt0sr  11229  addresr  11262  mulresr  11263  axaddf  11269  axmulf  11270  axaddass  11280  axmulass  11281  axdistr  11282  mulgt0  11426  mul4  11517  add4  11570  2addsub  11610  addsubeq4  11611  sub4  11642  muladd  11787  mulsub  11798  mulge0  11874  add20i  11899  mulge0i  11903  mulne0  11998  divmuldiv  12057  rec11i  12098  ltmul12a  12213  mulge0b  12227  zmulcl  12785  uz2mulcl  13093  qaddcl  13133  qmulcl  13135  qreccl  13137  rpaddcl  13184  xmulgt0  13453  xmulge0  13454  ixxin  13533  ge0addcl  13631  ge0xaddcl  13633  fzadd2  13733  serge0  14239  expge1  14282  sqrmo  15461  rexanuz  15557  amgm2  15581  bhmafibid1cn  15677  bhmafibid2cn  15678  mulcn2  15807  dvds2ln  16503  opoe  16577  omoe  16578  opeo  16579  omeo  16580  divalglem6  16612  divalglem8  16614  lcmcllem  16815  lcmgcd  16826  lcmdvds  16827  pc2dvds  17101  catpropd  17933  gimco  19532  efgrelexlemb  20015  rimco  20798  isdrng5  21059  psgnghm  21941  pf1ind  22728  tgcl  23342  innei  23498  iunconnlem  23800  txbas  23941  txss12  23979  txbasval  23980  tx1stc  24024  fbunfip  24243  tsmsxp  24529  blsscls2  24878  bddnghm  25100  qtopbaslem  25132  iimulcl  25313  icoopnst  25315  iocopnst  25316  iccpnfcnv  25320  mumullem2  27564  fsumvma  27597  lgslem3  27683  pntrsumbnd2  27951  mulsuniflem  28592  readdscl  28942  remulscllem2  28944  remulscl  28945  ajmoi  31517  hvadd4  31695  hvsub4  31696  shsel3  31974  shscli  31976  shscom  31978  chj4  32194  5oalem3  32315  5oalem5  32317  5oalem6  32318  hoadd4  32443  adjmo  32491  adjsym  32492  cnvadj  32551  leopmuli  32792  mdslmd1lem2  32985  chirredlem2  33050  chirredi  33053  cdjreui  33091  addltmulALT  33147  reofld  34008  xrge0iifcnv  34676  dfac16  35887  funtransport  37011  btwnconn1lem13  37079  btwnconn1lem14  37080  outsideofeu  37111  outsidele  37112  funray  37120  lineintmo  37137  nmuladdss  37177  bj-nnfan  37871  bj-nnfor  37873  icoreclin  38548  poimirlem27  38833  heicant  38841  itg2gt0cn  38861  bndss  38986  isdrngo3  39159  riscer  39188  intidl  39229  unxpwdom3  44363  gbegt5  49132