Theorem an4s 666

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  an42s  667  anandis  684  anandirs  685  ax13  2383  nfeqf  2389  frminex  5597  trin2  6073  funprg  6539  funcnvqp  6549  fnun  6599  2elresin  6606  f1cof1  6733  f1oun  6786  f1oco  6790  fvreseq0  6979  f1mpt  7205  poxp  8068  soxp  8069  poseq  8098  wfr3g  8259  tfrlem7  8312  oeoe  8525  brecop  8747  pmss12g  8807  dif1ennnALT  9177  fiin  9325  tcmin  9651  frr3g  9671  harval2  9912  genpv  10913  genpdm  10916  genpnnp  10919  genpcd  10920  genpnmax  10921  addcmpblnr  10983  ltsrpr  10991  addclsr  10997  mulclsr  10998  addasssr  11002  mulasssr  11004  distrsr  11005  mulgt0sr  11019  addresr  11052  mulresr  11053  axaddf  11059  axmulf  11060  axaddass  11070  axmulass  11071  axdistr  11072  mulgt0  11214  mul4  11305  add4  11358  2addsub  11398  addsubeq4  11399  sub4  11430  muladd  11573  mulsub  11584  mulge0  11659  add20i  11684  mulge0i  11688  mulne0  11783  divmuldiv  11846  rec11i  11887  ltmul12a  12002  mulge0b  12017  zmulcl  12567  uz2mulcl  12867  qaddcl  12906  qmulcl  12908  qreccl  12910  rpaddcl  12957  xmulgt0  13226  xmulge0  13227  ixxin  13306  ge0addcl  13404  ge0xaddcl  13406  fzadd2  13504  serge0  14009  expge1  14052  sqrmo  15204  rexanuz  15299  amgm2  15323  bhmafibid1cn  15419  bhmafibid2cn  15420  mulcn2  15549  dvds2ln  16249  opoe  16323  omoe  16324  opeo  16325  omeo  16326  divalglem6  16358  divalglem8  16360  lcmcllem  16556  lcmgcd  16567  lcmdvds  16568  pc2dvds  16841  catpropd  17666  gimco  19234  efgrelexlemb  19716  psgnghm  21555  pf1ind  22341  tgcl  22952  innei  23108  iunconnlem  23410  txbas  23550  txss12  23588  txbasval  23589  tx1stc  23633  fbunfip  23852  tsmsxp  24138  blsscls2  24487  bddnghm  24709  qtopbaslem  24741  iimulcl  24922  icoopnst  24924  iocopnst  24925  iccpnfcnv  24929  mumullem2  27161  fsumvma  27194  lgslem3  27280  pntrsumbnd2  27548  mulsuniflem  28159  readdscl  28509  remulscllem2  28511  remulscl  28512  ajmoi  30947  hvadd4  31125  hvsub4  31126  shsel3  31404  shscli  31406  shscom  31408  chj4  31624  5oalem3  31745  5oalem5  31747  5oalem6  31748  hoadd4  31873  adjmo  31921  adjsym  31922  cnvadj  31981  leopmuli  32222  mdslmd1lem2  32415  chirredlem2  32480  chirredi  32483  cdjreui  32521  addltmulALT  32535  reofld  33426  xrge0iifcnv  34117  funtransport  36259  btwnconn1lem13  36327  btwnconn1lem14  36328  outsideofeu  36359  outsidele  36360  funray  36368  lineintmo  36385  bj-nnfan  37097  bj-nnfor  37099  icoreclin  37719  poimirlem27  38014  heicant  38022  itg2gt0cn  38042  bndss  38153  isdrngo3  38326  riscer  38355  intidl  38396  rimco  43005  unxpwdom3  43540  gbegt5  48252