Theorem an4s 660

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 656	. 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  661  anandis  678  anandirs  679  ax13  2373  nfeqf  2379  frminex  5610  trin2  6084  funprg  6554  funcnvqp  6564  fnun  6614  2elresin  6621  f1cof1  6748  f1oun  6801  f1oco  6805  fvreseq0  6992  f1mpt  7218  poxp  8084  soxp  8085  poseq  8114  wfr3g  8275  tfrlem7  8328  oeoe  8540  brecop  8760  pmss12g  8819  dif1ennnALT  9198  fiin  9349  tcmin  9670  frr3g  9685  harval2  9926  genpv  10928  genpdm  10931  genpnnp  10934  genpcd  10935  genpnmax  10936  addcmpblnr  10998  ltsrpr  11006  addclsr  11012  mulclsr  11013  addasssr  11017  mulasssr  11019  distrsr  11020  mulgt0sr  11034  addresr  11067  mulresr  11068  axaddf  11074  axmulf  11075  axaddass  11085  axmulass  11086  axdistr  11087  mulgt0  11227  mul4  11318  add4  11371  2addsub  11411  addsubeq4  11412  sub4  11443  muladd  11586  mulsub  11597  mulge0  11672  add20i  11697  mulge0i  11701  mulne0  11796  divmuldiv  11858  rec11i  11899  ltmul12a  12014  mulge0b  12029  zmulcl  12558  uz2mulcl  12861  qaddcl  12900  qmulcl  12902  qreccl  12904  rpaddcl  12951  xmulgt0  13219  xmulge0  13220  ixxin  13299  ge0addcl  13397  ge0xaddcl  13399  fzadd2  13496  serge0  13997  expge1  14040  sqrmo  15193  rexanuz  15288  amgm2  15312  bhmafibid1cn  15408  bhmafibid2cn  15409  mulcn2  15538  dvds2ln  16235  opoe  16309  omoe  16310  opeo  16311  omeo  16312  divalglem6  16344  divalglem8  16346  lcmcllem  16542  lcmgcd  16553  lcmdvds  16554  pc2dvds  16826  catpropd  17650  gimco  19182  efgrelexlemb  19664  psgnghm  21522  pf1ind  22275  tgcl  22889  innei  23045  iunconnlem  23347  txbas  23487  txss12  23525  txbasval  23526  tx1stc  23570  fbunfip  23789  tsmsxp  24075  blsscls2  24425  bddnghm  24647  qtopbaslem  24679  iimulcl  24866  icoopnst  24869  iocopnst  24870  iccpnfcnv  24875  mumullem2  27123  fsumvma  27157  lgslem3  27243  pntrsumbnd2  27511  mulsuniflem  28092  readdscl  28403  remulscllem2  28405  remulscl  28406  ajmoi  30837  hvadd4  31015  hvsub4  31016  shsel3  31294  shscli  31296  shscom  31298  chj4  31514  5oalem3  31635  5oalem5  31637  5oalem6  31638  hoadd4  31763  adjmo  31811  adjsym  31812  cnvadj  31871  leopmuli  32112  mdslmd1lem2  32305  chirredlem2  32370  chirredi  32373  cdjreui  32411  addltmulALT  32425  reofld  33308  xrge0iifcnv  33916  funtransport  36012  btwnconn1lem13  36080  btwnconn1lem14  36081  outsideofeu  36112  outsidele  36113  funray  36121  lineintmo  36138  bj-nnfan  36729  bj-nnfor  36731  icoreclin  37338  poimirlem27  37634  heicant  37642  itg2gt0cn  37662  bndss  37773  isdrngo3  37946  riscer  37975  intidl  38016  rimco  42499  unxpwdom3  43077  gbegt5  47755