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  2377  nfeqf  2383  frminex  5667  trin2  6145  funprg  6621  funcnvqp  6631  fnun  6682  2elresin  6689  f1cof1  6814  f1oun  6867  f1oco  6871  fvreseq0  7057  f1mpt  7280  poxp  8151  soxp  8152  poseq  8181  wfr3g  8345  wfrfunOLD  8357  tfrlem7  8421  oeoe  8635  brecop  8848  pmss12g  8907  dif1ennnALT  9308  fiin  9459  tcmin  9778  frr3g  9793  harval2  10034  genpv  11036  genpdm  11039  genpnnp  11042  genpcd  11043  genpnmax  11044  addcmpblnr  11106  ltsrpr  11114  addclsr  11120  mulclsr  11121  addasssr  11125  mulasssr  11127  distrsr  11128  mulgt0sr  11142  addresr  11175  mulresr  11176  axaddf  11182  axmulf  11183  axaddass  11193  axmulass  11194  axdistr  11195  mulgt0  11335  mul4  11426  add4  11479  2addsub  11519  addsubeq4  11520  sub4  11551  muladd  11692  mulsub  11703  mulge0  11778  add20i  11803  mulge0i  11807  mulne0  11902  divmuldiv  11964  rec11i  12005  ltmul12a  12120  mulge0b  12135  zmulcl  12663  uz2mulcl  12965  qaddcl  13004  qmulcl  13006  qreccl  13008  rpaddcl  13054  xmulgt0  13321  xmulge0  13322  ixxin  13400  ge0addcl  13496  ge0xaddcl  13498  fzadd2  13595  serge0  14093  expge1  14136  sqrmo  15286  rexanuz  15380  amgm2  15404  bhmafibid1cn  15498  bhmafibid2cn  15499  mulcn2  15628  dvds2ln  16322  opoe  16396  omoe  16397  opeo  16398  omeo  16399  divalglem6  16431  divalglem8  16433  lcmcllem  16629  lcmgcd  16640  lcmdvds  16641  pc2dvds  16912  catpropd  17753  gimco  19298  efgrelexlemb  19782  psgnghm  21615  pf1ind  22374  tgcl  22991  innei  23148  iunconnlem  23450  txbas  23590  txss12  23628  txbasval  23629  tx1stc  23673  fbunfip  23892  tsmsxp  24178  blsscls2  24532  bddnghm  24762  qtopbaslem  24794  iimulcl  24979  icoopnst  24982  iocopnst  24983  iccpnfcnv  24988  mumullem2  27237  fsumvma  27271  lgslem3  27357  pntrsumbnd2  27625  mulsuniflem  28189  readdscl  28445  remulscllem2  28447  remulscl  28448  ajmoi  30886  hvadd4  31064  hvsub4  31065  shsel3  31343  shscli  31345  shscom  31347  chj4  31563  5oalem3  31684  5oalem5  31686  5oalem6  31687  hoadd4  31812  adjmo  31860  adjsym  31861  cnvadj  31920  leopmuli  32161  mdslmd1lem2  32354  chirredlem2  32419  chirredi  32422  cdjreui  32460  addltmulALT  32474  reofld  33351  xrge0iifcnv  33893  funtransport  36012  btwnconn1lem13  36080  btwnconn1lem14  36081  outsideofeu  36112  outsidele  36113  funray  36121  lineintmo  36138  bj-nnfan  36730  bj-nnfor  36732  icoreclin  37339  poimirlem27  37633  heicant  37641  itg2gt0cn  37661  bndss  37772  isdrngo3  37945  riscer  37974  intidl  38015  rimco  42504  unxpwdom3  43083  gbegt5  47685