Theorem an4s 659

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 655	. 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  660  anandis  677  anandirs  678  ax13  2383  nfeqf  2389  frminex  5679  trin2  6155  funprg  6632  funcnvqp  6642  fnun  6693  2elresin  6701  f1cof1  6827  f1coOLD  6829  f1oun  6881  f1oco  6885  fvreseq0  7071  f1mpt  7298  poxp  8169  soxp  8170  poseq  8199  wfr3g  8363  wfrfunOLD  8375  tfrlem7  8439  oeoe  8655  brecop  8868  pmss12g  8927  dif1ennnALT  9339  fiin  9491  tcmin  9810  frr3g  9825  harval2  10066  genpv  11068  genpdm  11071  genpnnp  11074  genpcd  11075  genpnmax  11076  addcmpblnr  11138  ltsrpr  11146  addclsr  11152  mulclsr  11153  addasssr  11157  mulasssr  11159  distrsr  11160  mulgt0sr  11174  addresr  11207  mulresr  11208  axaddf  11214  axmulf  11215  axaddass  11225  axmulass  11226  axdistr  11227  mulgt0  11367  mul4  11458  add4  11510  2addsub  11550  addsubeq4  11551  sub4  11581  muladd  11722  mulsub  11733  mulge0  11808  add20i  11833  mulge0i  11837  mulne0  11932  divmuldiv  11994  rec11i  12035  ltmul12a  12150  mulge0b  12165  zmulcl  12692  uz2mulcl  12991  qaddcl  13030  qmulcl  13032  qreccl  13034  rpaddcl  13079  xmulgt0  13345  xmulge0  13346  ixxin  13424  ge0addcl  13520  ge0xaddcl  13522  fzadd2  13619  serge0  14107  expge1  14150  sqrmo  15300  rexanuz  15394  amgm2  15418  bhmafibid1cn  15512  bhmafibid2cn  15513  mulcn2  15642  dvds2ln  16337  opoe  16411  omoe  16412  opeo  16413  omeo  16414  divalglem6  16446  divalglem8  16448  lcmcllem  16643  lcmgcd  16654  lcmdvds  16655  pc2dvds  16926  catpropd  17767  gimco  19308  efgrelexlemb  19792  psgnghm  21621  pf1ind  22380  tgcl  22997  innei  23154  iunconnlem  23456  txbas  23596  txss12  23634  txbasval  23635  tx1stc  23679  fbunfip  23898  tsmsxp  24184  blsscls2  24538  bddnghm  24768  qtopbaslem  24800  iimulcl  24985  icoopnst  24988  iocopnst  24989  iccpnfcnv  24994  mumullem2  27241  fsumvma  27275  lgslem3  27361  pntrsumbnd2  27629  mulsuniflem  28193  readdscl  28449  remulscllem2  28451  remulscl  28452  ajmoi  30890  hvadd4  31068  hvsub4  31069  shsel3  31347  shscli  31349  shscom  31351  chj4  31567  5oalem3  31688  5oalem5  31690  5oalem6  31691  hoadd4  31816  adjmo  31864  adjsym  31865  cnvadj  31924  leopmuli  32165  mdslmd1lem2  32358  chirredlem2  32423  chirredi  32426  cdjreui  32464  addltmulALT  32478  reofld  33337  xrge0iifcnv  33879  funtransport  35995  btwnconn1lem13  36063  btwnconn1lem14  36064  outsideofeu  36095  outsidele  36096  funray  36104  lineintmo  36121  bj-nnfan  36714  bj-nnfor  36716  icoreclin  37323  poimirlem27  37607  heicant  37615  itg2gt0cn  37635  bndss  37746  isdrngo3  37919  riscer  37948  intidl  37989  rimco  42473  unxpwdom3  43052  gbegt5  47635