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  2379  nfeqf  2385  frminex  5603  trin2  6080  funprg  6546  funcnvqp  6556  fnun  6606  2elresin  6613  f1cof1  6740  f1oun  6793  f1oco  6797  fvreseq0  6983  f1mpt  7207  poxp  8070  soxp  8071  poseq  8100  wfr3g  8261  tfrlem7  8314  oeoe  8527  brecop  8747  pmss12g  8807  dif1ennnALT  9177  fiin  9325  tcmin  9648  frr3g  9668  harval2  9909  genpv  10910  genpdm  10913  genpnnp  10916  genpcd  10917  genpnmax  10918  addcmpblnr  10980  ltsrpr  10988  addclsr  10994  mulclsr  10995  addasssr  10999  mulasssr  11001  distrsr  11002  mulgt0sr  11016  addresr  11049  mulresr  11050  axaddf  11056  axmulf  11057  axaddass  11067  axmulass  11068  axdistr  11069  mulgt0  11210  mul4  11301  add4  11354  2addsub  11394  addsubeq4  11395  sub4  11426  muladd  11569  mulsub  11580  mulge0  11655  add20i  11680  mulge0i  11684  mulne0  11779  divmuldiv  11841  rec11i  11882  ltmul12a  11997  mulge0b  12012  zmulcl  12540  uz2mulcl  12839  qaddcl  12878  qmulcl  12880  qreccl  12882  rpaddcl  12929  xmulgt0  13198  xmulge0  13199  ixxin  13278  ge0addcl  13376  ge0xaddcl  13378  fzadd2  13475  serge0  13979  expge1  14022  sqrmo  15174  rexanuz  15269  amgm2  15293  bhmafibid1cn  15389  bhmafibid2cn  15390  mulcn2  15519  dvds2ln  16216  opoe  16290  omoe  16291  opeo  16292  omeo  16293  divalglem6  16325  divalglem8  16327  lcmcllem  16523  lcmgcd  16534  lcmdvds  16535  pc2dvds  16807  catpropd  17632  gimco  19197  efgrelexlemb  19679  psgnghm  21535  pf1ind  22299  tgcl  22913  innei  23069  iunconnlem  23371  txbas  23511  txss12  23549  txbasval  23550  tx1stc  23594  fbunfip  23813  tsmsxp  24099  blsscls2  24448  bddnghm  24670  qtopbaslem  24702  iimulcl  24889  icoopnst  24892  iocopnst  24893  iccpnfcnv  24898  mumullem2  27146  fsumvma  27180  lgslem3  27266  pntrsumbnd2  27534  mulsuniflem  28145  readdscl  28495  remulscllem2  28497  remulscl  28498  ajmoi  30933  hvadd4  31111  hvsub4  31112  shsel3  31390  shscli  31392  shscom  31394  chj4  31610  5oalem3  31731  5oalem5  31733  5oalem6  31734  hoadd4  31859  adjmo  31907  adjsym  31908  cnvadj  31967  leopmuli  32208  mdslmd1lem2  32401  chirredlem2  32466  chirredi  32469  cdjreui  32507  addltmulALT  32521  reofld  33424  xrge0iifcnv  34090  funtransport  36225  btwnconn1lem13  36293  btwnconn1lem14  36294  outsideofeu  36325  outsidele  36326  funray  36334  lineintmo  36351  bj-nnfan  36949  bj-nnfor  36951  icoreclin  37562  poimirlem27  37848  heicant  37856  itg2gt0cn  37876  bndss  37987  isdrngo3  38160  riscer  38189  intidl  38230  rimco  42773  unxpwdom3  43337  gbegt5  48007