Theorem an4s 658

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  an42s  659  anandis  676  anandirs  677  ax13  2393  nfeqf  2399  frminex  5537  trin2  5985  funprg  6410  funcnvqp  6420  fnun  6465  2elresin  6470  f1co  6587  f1oun  6636  f1oco  6639  fvreseq0  6810  f1mpt  7021  poxp  7824  soxp  7825  wfr3g  7955  wfrfun  7967  tfrlem7  8021  oeoe  8227  brecop  8392  pmss12g  8435  dif1en  8753  fiin  8888  tcmin  9185  harval2  9428  genpv  10423  genpdm  10426  genpnnp  10429  genpcd  10430  genpnmax  10431  addcmpblnr  10493  ltsrpr  10501  addclsr  10507  mulclsr  10508  addasssr  10512  mulasssr  10514  distrsr  10515  mulgt0sr  10529  addresr  10562  mulresr  10563  axaddf  10569  axmulf  10570  axaddass  10580  axmulass  10581  axdistr  10582  mulgt0  10720  mul4  10810  add4  10862  2addsub  10902  addsubeq4  10903  sub4  10933  muladd  11074  mulsub  11085  mulge0  11160  add20i  11185  mulge0i  11189  mulne0  11284  divmuldiv  11342  rec11i  11383  ltmul12a  11498  mulge0b  11512  zmulcl  12034  uz2mulcl  12329  qaddcl  12367  qmulcl  12369  qreccl  12371  rpaddcl  12414  xmulgt0  12679  xmulge0  12680  ixxin  12758  ge0addcl  12851  ge0xaddcl  12853  fzadd2  12945  serge0  13427  expge1  13469  sqrmo  14613  rexanuz  14707  amgm2  14731  bhmafibid1cn  14825  bhmafibid2cn  14826  mulcn2  14954  dvds2ln  15644  opoe  15714  omoe  15715  opeo  15716  omeo  15717  divalglem6  15751  divalglem8  15753  lcmcllem  15942  lcmgcd  15953  lcmdvds  15954  pc2dvds  16217  catpropd  16981  gimco  18410  efgrelexlemb  18878  pf1ind  20520  psgnghm  20726  tgcl  21579  innei  21735  iunconnlem  22037  txbas  22177  txss12  22215  txbasval  22216  tx1stc  22260  fbunfip  22479  tsmsxp  22765  blsscls2  23116  bddnghm  23337  qtopbaslem  23369  iimulcl  23543  icoopnst  23545  iocopnst  23546  iccpnfcnv  23550  mumullem2  25759  fsumvma  25791  lgslem3  25877  pntrsumbnd2  26145  ajmoi  28637  hvadd4  28815  hvsub4  28816  shsel3  29094  shscli  29096  shscom  29098  chj4  29314  5oalem3  29435  5oalem5  29437  5oalem6  29438  hoadd4  29563  adjmo  29611  adjsym  29612  cnvadj  29671  leopmuli  29912  mdslmd1lem2  30105  chirredlem2  30170  chirredi  30173  cdjreui  30211  addltmulALT  30225  reofld  30915  xrge0iifcnv  31178  poseq  33097  frr3g  33123  funtransport  33494  btwnconn1lem13  33562  btwnconn1lem14  33563  outsideofeu  33594  outsidele  33595  funray  33603  lineintmo  33620  bj-nnfan  34079  bj-nnfor  34081  icoreclin  34640  poimirlem27  34921  heicant  34929  itg2gt0cn  34949  bndss  35066  isdrngo3  35239  riscer  35268  intidl  35309  unxpwdom3  39702  gbegt5  43933