Theorem an4s 869

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  an42s  870  anandis  873  anandirs  874  ax13  2249  nfeqf  2301  frminex  5094  trin2  5519  funprg  5940  funcnvqp  5952  fnun  5997  2elresin  6002  f1co  6110  f1oun  6156  f1oco  6159  fvreseq0  6317  f1mpt  6518  poxp  7289  soxp  7290  wfr3g  7413  wfrfun  7425  tfrlem7  7479  oeoe  7679  brecop  7840  pmss12g  7884  dif1en  8193  fiin  8328  tcmin  8617  harval2  8823  genpv  9821  genpdm  9824  genpnnp  9827  genpcd  9828  genpnmax  9829  addcmpblnr  9890  ltsrpr  9898  addclsr  9904  mulclsr  9905  addasssr  9909  mulasssr  9911  distrsr  9912  mulgt0sr  9926  addresr  9959  mulresr  9960  axaddf  9966  axmulf  9967  axaddass  9977  axmulass  9978  axdistr  9979  mulgt0  10115  mul4  10205  add4  10256  2addsub  10295  addsubeq4  10296  sub4  10326  muladd  10462  mulsub  10473  mulge0  10546  add20i  10571  mulge0i  10575  mulne0  10669  divmuldiv  10725  rec11i  10766  ltmul12a  10879  mulge0b  10893  zmulcl  11426  uz2mulcl  11766  qaddcl  11804  qmulcl  11806  qreccl  11808  rpaddcl  11854  xmulgt0  12113  xmulge0  12114  ixxin  12192  ge0addcl  12284  ge0xaddcl  12286  fzadd2  12376  serge0  12855  expge1  12897  sqrmo  13992  rexanuz  14085  amgm2  14109  mulcn2  14326  dvds2ln  15014  opoe  15087  omoe  15088  opeo  15089  omeo  15090  divalglem6  15121  divalglem8  15123  lcmcllem  15309  lcmgcd  15320  lcmdvds  15321  pc2dvds  15583  catpropd  16369  gimco  17710  efgrelexlemb  18163  pf1ind  19719  psgnghm  19926  tgcl  20773  innei  20929  iunconnlem  21230  txbas  21370  txss12  21408  txbasval  21409  tx1stc  21453  fbunfip  21673  tsmsxp  21958  blsscls2  22309  bddnghm  22530  qtopbaslem  22562  iimulcl  22736  icoopnst  22738  iocopnst  22739  iccpnfcnv  22743  mumullem2  24906  fsumvma  24938  lgslem3  25024  pntrsumbnd2  25256  wlknwwlksnfun  26774  ajmoi  27714  hvadd4  27893  hvsub4  27894  shsel3  28174  shscli  28176  shscom  28178  chj4  28394  5oalem3  28515  5oalem5  28517  5oalem6  28518  hoadd4  28643  adjmo  28691  adjsym  28692  cnvadj  28751  leopmuli  28992  mdslmd1lem2  29185  chirredlem2  29250  chirredi  29253  cdjreui  29291  addltmulALT  29305  reofld  29840  xrge0iifcnv  29979  poseq  31750  frr3g  31779  frrlem4  31783  frrlem5c  31786  funtransport  32138  btwnconn1lem13  32206  btwnconn1lem14  32207  outsideofeu  32238  outsidele  32239  funray  32247  lineintmo  32264  icoreclin  33205  poimirlem27  33436  heicant  33444  itg2gt0cn  33465  bndss  33585  isdrngo3  33758  riscer  33787  intidl  33828  unxpwdom3  37665  gbegt5  41649