Theorem an4s 670

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  an42s  671  anandis  688  anandirs  689  ax13  2406  nfeqf  2412  frminex  5626  trin2  6110  funprg  6575  funcnvqp  6585  fnun  6635  2elresin  6642  f1cof1  6772  f1oun  6826  f1oco  6830  fvreseq0  7019  f1mpt  7245  poxp  8108  soxp  8109  poseq  8138  wfr3g  8300  tfrlem7  8354  oeoe  8569  brecop  8792  pmss12g  8851  dif1ennnALT  9221  fiin  9368  tcmin  9694  frr3g  9714  harval2  9955  genpv  10957  genpdm  10960  genpnnp  10963  genpcd  10964  genpnmax  10965  addcmpblnr  11027  ltsrpr  11035  addclsr  11041  mulclsr  11042  addasssr  11046  mulasssr  11048  distrsr  11049  mulgt0sr  11063  addresr  11096  mulresr  11097  axaddf  11103  axmulf  11104  axaddass  11114  axmulass  11115  axdistr  11116  mulgt0  11260  mul4  11351  add4  11404  2addsub  11444  addsubeq4  11445  sub4  11476  muladd  11619  mulsub  11630  mulge0  11705  add20i  11730  mulge0i  11734  mulne0  11829  divmuldiv  11891  rec11i  11932  ltmul12a  12047  mulge0b  12062  zmulcl  12620  uz2mulcl  12927  qaddcl  12966  qmulcl  12968  qreccl  12970  rpaddcl  13017  xmulgt0  13286  xmulge0  13287  ixxin  13366  ge0addcl  13464  ge0xaddcl  13466  fzadd2  13564  serge0  14069  expge1  14112  sqrmo  15278  rexanuz  15373  amgm2  15397  bhmafibid1cn  15493  bhmafibid2cn  15494  mulcn2  15623  dvds2ln  16323  opoe  16397  omoe  16398  opeo  16399  omeo  16400  divalglem6  16432  divalglem8  16434  lcmcllem  16630  lcmgcd  16641  lcmdvds  16642  pc2dvds  16915  catpropd  17741  gimco  19308  efgrelexlemb  19790  psgnghm  21632  pf1ind  22418  tgcl  23029  innei  23185  iunconnlem  23487  txbas  23627  txss12  23665  txbasval  23666  tx1stc  23710  fbunfip  23929  tsmsxp  24215  blsscls2  24564  bddnghm  24786  qtopbaslem  24818  iimulcl  24999  icoopnst  25001  iocopnst  25002  iccpnfcnv  25006  mumullem2  27244  fsumvma  27277  lgslem3  27363  pntrsumbnd2  27631  mulsuniflem  28242  readdscl  28592  remulscllem2  28594  remulscl  28595  ajmoi  31061  hvadd4  31239  hvsub4  31240  shsel3  31518  shscli  31520  shscom  31522  chj4  31738  5oalem3  31859  5oalem5  31861  5oalem6  31862  hoadd4  31987  adjmo  32035  adjsym  32036  cnvadj  32095  leopmuli  32336  mdslmd1lem2  32529  chirredlem2  32594  chirredi  32597  cdjreui  32635  addltmulALT  32649  reofld  33529  xrge0iifcnv  34230  funtransport  36381  btwnconn1lem13  36449  btwnconn1lem14  36450  outsideofeu  36481  outsidele  36482  funray  36490  lineintmo  36507  bj-nnfan  37229  bj-nnfor  37231  icoreclin  37851  poimirlem27  38146  heicant  38154  itg2gt0cn  38174  bndss  38285  isdrngo3  38458  riscer  38487  intidl  38528  rimco  43137  unxpwdom3  43672  gbegt5  48383