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  2375  nfeqf  2381  frminex  5593  trin2  6069  funprg  6535  funcnvqp  6545  fnun  6595  2elresin  6602  f1cof1  6729  f1oun  6782  f1oco  6786  fvreseq0  6971  f1mpt  7195  poxp  8058  soxp  8059  poseq  8088  wfr3g  8249  tfrlem7  8302  oeoe  8514  brecop  8734  pmss12g  8793  dif1ennnALT  9161  fiin  9306  tcmin  9629  frr3g  9649  harval2  9890  genpv  10890  genpdm  10893  genpnnp  10896  genpcd  10897  genpnmax  10898  addcmpblnr  10960  ltsrpr  10968  addclsr  10974  mulclsr  10975  addasssr  10979  mulasssr  10981  distrsr  10982  mulgt0sr  10996  addresr  11029  mulresr  11030  axaddf  11036  axmulf  11037  axaddass  11047  axmulass  11048  axdistr  11049  mulgt0  11190  mul4  11281  add4  11334  2addsub  11374  addsubeq4  11375  sub4  11406  muladd  11549  mulsub  11560  mulge0  11635  add20i  11660  mulge0i  11664  mulne0  11759  divmuldiv  11821  rec11i  11862  ltmul12a  11977  mulge0b  11992  zmulcl  12521  uz2mulcl  12824  qaddcl  12863  qmulcl  12865  qreccl  12867  rpaddcl  12914  xmulgt0  13182  xmulge0  13183  ixxin  13262  ge0addcl  13360  ge0xaddcl  13362  fzadd2  13459  serge0  13963  expge1  14006  sqrmo  15158  rexanuz  15253  amgm2  15277  bhmafibid1cn  15373  bhmafibid2cn  15374  mulcn2  15503  dvds2ln  16200  opoe  16274  omoe  16275  opeo  16276  omeo  16277  divalglem6  16309  divalglem8  16311  lcmcllem  16507  lcmgcd  16518  lcmdvds  16519  pc2dvds  16791  catpropd  17615  gimco  19180  efgrelexlemb  19662  psgnghm  21517  pf1ind  22270  tgcl  22884  innei  23040  iunconnlem  23342  txbas  23482  txss12  23520  txbasval  23521  tx1stc  23565  fbunfip  23784  tsmsxp  24070  blsscls2  24419  bddnghm  24641  qtopbaslem  24673  iimulcl  24860  icoopnst  24863  iocopnst  24864  iccpnfcnv  24869  mumullem2  27117  fsumvma  27151  lgslem3  27237  pntrsumbnd2  27505  mulsuniflem  28088  readdscl  28401  remulscllem2  28403  remulscl  28404  ajmoi  30838  hvadd4  31016  hvsub4  31017  shsel3  31295  shscli  31297  shscom  31299  chj4  31515  5oalem3  31636  5oalem5  31638  5oalem6  31639  hoadd4  31764  adjmo  31812  adjsym  31813  cnvadj  31872  leopmuli  32113  mdslmd1lem2  32306  chirredlem2  32371  chirredi  32374  cdjreui  32412  addltmulALT  32426  reofld  33308  xrge0iifcnv  33946  funtransport  36075  btwnconn1lem13  36143  btwnconn1lem14  36144  outsideofeu  36175  outsidele  36176  funray  36184  lineintmo  36201  bj-nnfan  36792  bj-nnfor  36794  icoreclin  37401  poimirlem27  37697  heicant  37705  itg2gt0cn  37725  bndss  37836  isdrngo3  38009  riscer  38038  intidl  38079  rimco  42621  unxpwdom3  43198  gbegt5  47871