Theorem an4s 673

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an42s  674  anandis  691  anandirs  692  ax13  2405  nfeqf  2411  frminex  5630  trin2  6117  funprg  6594  funcnvqp  6604  fnun  6653  2elresin  6660  f1cof1  6790  f1oun  6844  f1oco  6848  fvreseq0  7037  f1mpt  7265  poxp  8140  soxp  8141  poseq  8175  wfr3g  8337  tfrlem7  8391  oeoe  8608  brecop  8831  pmss12g  8897  dif1ennnALT  9268  fiin  9414  tcmin  9740  frr3g  9760  harval2  10078  genpv  11084  genpdm  11087  genpnnp  11090  genpcd  11091  genpnmax  11092  addcmpblnr  11154  ltsrpr  11162  addclsr  11168  mulclsr  11169  addasssr  11173  mulasssr  11175  distrsr  11176  mulgt0sr  11190  addresr  11223  mulresr  11224  axaddf  11230  axmulf  11231  axaddass  11241  axmulass  11242  axdistr  11243  mulgt0  11387  mul4  11478  add4  11531  2addsub  11571  addsubeq4  11572  sub4  11603  muladd  11748  mulsub  11759  mulge0  11834  add20i  11859  mulge0i  11863  mulne0  11958  divmuldiv  12017  rec11i  12058  ltmul12a  12173  mulge0b  12187  zmulcl  12745  uz2mulcl  13053  qaddcl  13093  qmulcl  13095  qreccl  13097  rpaddcl  13144  xmulgt0  13413  xmulge0  13414  ixxin  13493  ge0addcl  13591  ge0xaddcl  13593  fzadd2  13693  serge0  14199  expge1  14242  sqrmo  15418  rexanuz  15513  amgm2  15537  bhmafibid1cn  15633  bhmafibid2cn  15634  mulcn2  15763  dvds2ln  16459  opoe  16533  omoe  16534  opeo  16535  omeo  16536  divalglem6  16568  divalglem8  16570  lcmcllem  16771  lcmgcd  16782  lcmdvds  16783  pc2dvds  17057  catpropd  17883  gimco  19482  efgrelexlemb  19964  rimco  20747  isdrng5  21008  psgnghm  21886  pf1ind  22673  tgcl  23287  innei  23443  iunconnlem  23745  txbas  23886  txss12  23924  txbasval  23925  tx1stc  23969  fbunfip  24188  tsmsxp  24474  blsscls2  24823  bddnghm  25045  qtopbaslem  25077  iimulcl  25258  icoopnst  25260  iocopnst  25261  iccpnfcnv  25265  mumullem2  27507  fsumvma  27540  lgslem3  27626  pntrsumbnd2  27894  mulsuniflem  28535  readdscl  28885  remulscllem2  28887  remulscl  28888  ajmoi  31460  hvadd4  31638  hvsub4  31639  shsel3  31917  shscli  31919  shscom  31921  chj4  32137  5oalem3  32258  5oalem5  32260  5oalem6  32261  hoadd4  32386  adjmo  32434  adjsym  32435  cnvadj  32494  leopmuli  32735  mdslmd1lem2  32928  chirredlem2  32993  chirredi  32996  cdjreui  33034  addltmulALT  33048  reofld  33904  xrge0iifcnv  34565  funtransport  36796  btwnconn1lem13  36864  btwnconn1lem14  36865  outsideofeu  36896  outsidele  36897  funray  36905  lineintmo  36922  nmuladdss  36962  bj-nnfan  37656  bj-nnfor  37658  icoreclin  38280  poimirlem27  38565  heicant  38573  itg2gt0cn  38593  bndss  38720  isdrngo3  38893  riscer  38922  intidl  38963  unxpwdom3  44096  gbegt5  48858