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  5601  trin2  6078  funprg  6544  funcnvqp  6554  fnun  6604  2elresin  6611  f1cof1  6738  f1oun  6791  f1oco  6795  fvreseq0  6981  f1mpt  7205  poxp  8068  soxp  8069  poseq  8098  wfr3g  8259  tfrlem7  8312  oeoe  8525  brecop  8745  pmss12g  8805  dif1ennnALT  9175  fiin  9323  tcmin  9646  frr3g  9666  harval2  9907  genpv  10908  genpdm  10911  genpnnp  10914  genpcd  10915  genpnmax  10916  addcmpblnr  10978  ltsrpr  10986  addclsr  10992  mulclsr  10993  addasssr  10997  mulasssr  10999  distrsr  11000  mulgt0sr  11014  addresr  11047  mulresr  11048  axaddf  11054  axmulf  11055  axaddass  11065  axmulass  11066  axdistr  11067  mulgt0  11208  mul4  11299  add4  11352  2addsub  11392  addsubeq4  11393  sub4  11424  muladd  11567  mulsub  11578  mulge0  11653  add20i  11678  mulge0i  11682  mulne0  11777  divmuldiv  11839  rec11i  11880  ltmul12a  11995  mulge0b  12010  zmulcl  12538  uz2mulcl  12837  qaddcl  12876  qmulcl  12878  qreccl  12880  rpaddcl  12927  xmulgt0  13196  xmulge0  13197  ixxin  13276  ge0addcl  13374  ge0xaddcl  13376  fzadd2  13473  serge0  13977  expge1  14020  sqrmo  15172  rexanuz  15267  amgm2  15291  bhmafibid1cn  15387  bhmafibid2cn  15388  mulcn2  15517  dvds2ln  16214  opoe  16288  omoe  16289  opeo  16290  omeo  16291  divalglem6  16323  divalglem8  16325  lcmcllem  16521  lcmgcd  16532  lcmdvds  16533  pc2dvds  16805  catpropd  17630  gimco  19195  efgrelexlemb  19677  psgnghm  21533  pf1ind  22297  tgcl  22911  innei  23067  iunconnlem  23369  txbas  23509  txss12  23547  txbasval  23548  tx1stc  23592  fbunfip  23811  tsmsxp  24097  blsscls2  24446  bddnghm  24668  qtopbaslem  24700  iimulcl  24887  icoopnst  24890  iocopnst  24891  iccpnfcnv  24896  mumullem2  27144  fsumvma  27178  lgslem3  27264  pntrsumbnd2  27532  mulsuniflem  28118  readdscl  28444  remulscllem2  28446  remulscl  28447  ajmoi  30882  hvadd4  31060  hvsub4  31061  shsel3  31339  shscli  31341  shscom  31343  chj4  31559  5oalem3  31680  5oalem5  31682  5oalem6  31683  hoadd4  31808  adjmo  31856  adjsym  31857  cnvadj  31916  leopmuli  32157  mdslmd1lem2  32350  chirredlem2  32415  chirredi  32418  cdjreui  32456  addltmulALT  32470  reofld  33373  xrge0iifcnv  34039  funtransport  36174  btwnconn1lem13  36242  btwnconn1lem14  36243  outsideofeu  36274  outsidele  36275  funray  36283  lineintmo  36300  bj-nnfan  36892  bj-nnfor  36894  icoreclin  37501  poimirlem27  37787  heicant  37795  itg2gt0cn  37815  bndss  37926  isdrngo3  38099  riscer  38128  intidl  38169  rimco  42715  unxpwdom3  43279  gbegt5  47949