Theorem an4s 661

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an42s  662  anandis  679  anandirs  680  ax13  2380  nfeqf  2386  frminex  5611  trin2  6088  funprg  6554  funcnvqp  6564  fnun  6614  2elresin  6621  f1cof1  6748  f1oun  6801  f1oco  6805  fvreseq0  6992  f1mpt  7217  poxp  8080  soxp  8081  poseq  8110  wfr3g  8271  tfrlem7  8324  oeoe  8537  brecop  8759  pmss12g  8819  dif1ennnALT  9189  fiin  9337  tcmin  9660  frr3g  9680  harval2  9921  genpv  10922  genpdm  10925  genpnnp  10928  genpcd  10929  genpnmax  10930  addcmpblnr  10992  ltsrpr  11000  addclsr  11006  mulclsr  11007  addasssr  11011  mulasssr  11013  distrsr  11014  mulgt0sr  11028  addresr  11061  mulresr  11062  axaddf  11068  axmulf  11069  axaddass  11079  axmulass  11080  axdistr  11081  mulgt0  11222  mul4  11313  add4  11366  2addsub  11406  addsubeq4  11407  sub4  11438  muladd  11581  mulsub  11592  mulge0  11667  add20i  11692  mulge0i  11696  mulne0  11791  divmuldiv  11853  rec11i  11894  ltmul12a  12009  mulge0b  12024  zmulcl  12552  uz2mulcl  12851  qaddcl  12890  qmulcl  12892  qreccl  12894  rpaddcl  12941  xmulgt0  13210  xmulge0  13211  ixxin  13290  ge0addcl  13388  ge0xaddcl  13390  fzadd2  13487  serge0  13991  expge1  14034  sqrmo  15186  rexanuz  15281  amgm2  15305  bhmafibid1cn  15401  bhmafibid2cn  15402  mulcn2  15531  dvds2ln  16228  opoe  16302  omoe  16303  opeo  16304  omeo  16305  divalglem6  16337  divalglem8  16339  lcmcllem  16535  lcmgcd  16546  lcmdvds  16547  pc2dvds  16819  catpropd  17644  gimco  19209  efgrelexlemb  19691  psgnghm  21547  pf1ind  22311  tgcl  22925  innei  23081  iunconnlem  23383  txbas  23523  txss12  23561  txbasval  23562  tx1stc  23606  fbunfip  23825  tsmsxp  24111  blsscls2  24460  bddnghm  24682  qtopbaslem  24714  iimulcl  24901  icoopnst  24904  iocopnst  24905  iccpnfcnv  24910  mumullem2  27158  fsumvma  27192  lgslem3  27278  pntrsumbnd2  27546  mulsuniflem  28157  readdscl  28507  remulscllem2  28509  remulscl  28510  ajmoi  30946  hvadd4  31124  hvsub4  31125  shsel3  31403  shscli  31405  shscom  31407  chj4  31623  5oalem3  31744  5oalem5  31746  5oalem6  31747  hoadd4  31872  adjmo  31920  adjsym  31921  cnvadj  31980  leopmuli  32221  mdslmd1lem2  32414  chirredlem2  32479  chirredi  32482  cdjreui  32520  addltmulALT  32534  reofld  33436  xrge0iifcnv  34111  funtransport  36247  btwnconn1lem13  36315  btwnconn1lem14  36316  outsideofeu  36347  outsidele  36348  funray  36356  lineintmo  36373  bj-nnfan  36997  bj-nnfor  36999  icoreclin  37612  poimirlem27  37898  heicant  37906  itg2gt0cn  37926  bndss  38037  isdrngo3  38210  riscer  38239  intidl  38280  rimco  42888  unxpwdom3  43452  gbegt5  48121