Theorem an4s 904

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

Syntax hints:   → wi 4   ∧ wa 383

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 385

This theorem is referenced by:  an42s  905  anandis  908  anandirs  909  ax13  2394  nfeqf  2446  frminex  5246  trin2  5677  funprg  6101  funcnvqp  6113  fnun  6158  2elresin  6163  f1co  6272  f1oun  6318  f1oco  6321  fvreseq0  6481  f1mpt  6682  poxp  7458  soxp  7459  wfr3g  7583  wfrfun  7595  tfrlem7  7649  oeoe  7850  brecop  8009  pmss12g  8052  dif1en  8360  fiin  8495  tcmin  8792  harval2  9033  genpv  10033  genpdm  10036  genpnnp  10039  genpcd  10040  genpnmax  10041  addcmpblnr  10102  ltsrpr  10110  addclsr  10116  mulclsr  10117  addasssr  10121  mulasssr  10123  distrsr  10124  mulgt0sr  10138  addresr  10171  mulresr  10172  axaddf  10178  axmulf  10179  axaddass  10189  axmulass  10190  axdistr  10191  mulgt0  10327  mul4  10417  add4  10468  2addsub  10507  addsubeq4  10508  sub4  10538  muladd  10674  mulsub  10685  mulge0  10758  add20i  10783  mulge0i  10787  mulne0  10881  divmuldiv  10937  rec11i  10978  ltmul12a  11091  mulge0b  11105  zmulcl  11638  uz2mulcl  11979  qaddcl  12017  qmulcl  12019  qreccl  12021  rpaddcl  12067  xmulgt0  12326  xmulge0  12327  ixxin  12405  ge0addcl  12497  ge0xaddcl  12499  fzadd2  12589  serge0  13069  expge1  13111  sqrmo  14211  rexanuz  14304  amgm2  14328  mulcn2  14545  dvds2ln  15236  opoe  15309  omoe  15310  opeo  15311  omeo  15312  divalglem6  15343  divalglem8  15345  lcmcllem  15531  lcmgcd  15542  lcmdvds  15543  pc2dvds  15805  catpropd  16590  gimco  17931  efgrelexlemb  18383  pf1ind  19941  psgnghm  20148  tgcl  20995  innei  21151  iunconnlem  21452  txbas  21592  txss12  21630  txbasval  21631  tx1stc  21675  fbunfip  21894  tsmsxp  22179  blsscls2  22530  bddnghm  22751  qtopbaslem  22783  iimulcl  22957  icoopnst  22959  iocopnst  22960  iccpnfcnv  22964  mumullem2  25126  fsumvma  25158  lgslem3  25244  pntrsumbnd2  25476  wlknwwlksnfun  27018  ajmoi  28044  hvadd4  28223  hvsub4  28224  shsel3  28504  shscli  28506  shscom  28508  chj4  28724  5oalem3  28845  5oalem5  28847  5oalem6  28848  hoadd4  28973  adjmo  29021  adjsym  29022  cnvadj  29081  leopmuli  29322  mdslmd1lem2  29515  chirredlem2  29580  chirredi  29583  cdjreui  29621  addltmulALT  29635  reofld  30170  xrge0iifcnv  30309  poseq  32080  frr3g  32106  frrlem5c  32113  funtransport  32465  btwnconn1lem13  32533  btwnconn1lem14  32534  outsideofeu  32565  outsidele  32566  funray  32574  lineintmo  32591  icoreclin  33534  poimirlem27  33767  heicant  33775  itg2gt0cn  33796  bndss  33916  isdrngo3  34089  riscer  34118  intidl  34159  unxpwdom3  38185  gbegt5  42177