Theorem an4s 657

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  an42s  658  anandis  675  anandirs  676  ax13  2375  nfeqf  2381  frminex  5569  trin2  6028  funprg  6488  funcnvqp  6498  fnun  6545  2elresin  6553  f1cof1  6681  f1coOLD  6683  f1oun  6735  f1oco  6739  fvreseq0  6915  f1mpt  7134  poxp  7969  soxp  7970  wfr3g  8138  wfrfunOLD  8150  tfrlem7  8214  oeoe  8430  brecop  8599  pmss12g  8657  dif1enALT  9050  fiin  9181  tcmin  9499  frr3g  9514  harval2  9755  genpv  10755  genpdm  10758  genpnnp  10761  genpcd  10762  genpnmax  10763  addcmpblnr  10825  ltsrpr  10833  addclsr  10839  mulclsr  10840  addasssr  10844  mulasssr  10846  distrsr  10847  mulgt0sr  10861  addresr  10894  mulresr  10895  axaddf  10901  axmulf  10902  axaddass  10912  axmulass  10913  axdistr  10914  mulgt0  11052  mul4  11143  add4  11195  2addsub  11235  addsubeq4  11236  sub4  11266  muladd  11407  mulsub  11418  mulge0  11493  add20i  11518  mulge0i  11522  mulne0  11617  divmuldiv  11675  rec11i  11716  ltmul12a  11831  mulge0b  11845  zmulcl  12369  uz2mulcl  12666  qaddcl  12705  qmulcl  12707  qreccl  12709  rpaddcl  12752  xmulgt0  13017  xmulge0  13018  ixxin  13096  ge0addcl  13192  ge0xaddcl  13194  fzadd2  13291  serge0  13777  expge1  13820  sqrmo  14963  rexanuz  15057  amgm2  15081  bhmafibid1cn  15175  bhmafibid2cn  15176  mulcn2  15305  dvds2ln  15998  opoe  16072  omoe  16073  opeo  16074  omeo  16075  divalglem6  16107  divalglem8  16109  lcmcllem  16301  lcmgcd  16312  lcmdvds  16313  pc2dvds  16580  catpropd  17418  gimco  18884  efgrelexlemb  19356  psgnghm  20785  pf1ind  21521  tgcl  22119  innei  22276  iunconnlem  22578  txbas  22718  txss12  22756  txbasval  22757  tx1stc  22801  fbunfip  23020  tsmsxp  23306  blsscls2  23660  bddnghm  23890  qtopbaslem  23922  iimulcl  24100  icoopnst  24102  iocopnst  24103  iccpnfcnv  24107  mumullem2  26329  fsumvma  26361  lgslem3  26447  pntrsumbnd2  26715  ajmoi  29220  hvadd4  29398  hvsub4  29399  shsel3  29677  shscli  29679  shscom  29681  chj4  29897  5oalem3  30018  5oalem5  30020  5oalem6  30021  hoadd4  30146  adjmo  30194  adjsym  30195  cnvadj  30254  leopmuli  30495  mdslmd1lem2  30688  chirredlem2  30753  chirredi  30756  cdjreui  30794  addltmulALT  30808  reofld  31544  xrge0iifcnv  31883  poseq  33802  funtransport  34333  btwnconn1lem13  34401  btwnconn1lem14  34402  outsideofeu  34433  outsidele  34434  funray  34442  lineintmo  34459  bj-nnfan  34930  bj-nnfor  34932  icoreclin  35528  poimirlem27  35804  heicant  35812  itg2gt0cn  35832  bndss  35944  isdrngo3  36117  riscer  36146  intidl  36187  unxpwdom3  40920  gbegt5  45213