Theorem an4s 658

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  an42s  659  anandis  676  anandirs  677  ax13  2392  nfeqf  2398  frminex  5538  trin2  5986  funprg  6411  funcnvqp  6421  fnun  6466  2elresin  6471  f1co  6588  f1oun  6637  f1oco  6640  fvreseq0  6811  f1mpt  7022  poxp  7825  soxp  7826  wfr3g  7956  wfrfun  7968  tfrlem7  8022  oeoe  8228  brecop  8393  pmss12g  8436  dif1en  8754  fiin  8889  tcmin  9186  harval2  9429  genpv  10424  genpdm  10427  genpnnp  10430  genpcd  10431  genpnmax  10432  addcmpblnr  10494  ltsrpr  10502  addclsr  10508  mulclsr  10509  addasssr  10513  mulasssr  10515  distrsr  10516  mulgt0sr  10530  addresr  10563  mulresr  10564  axaddf  10570  axmulf  10571  axaddass  10581  axmulass  10582  axdistr  10583  mulgt0  10721  mul4  10811  add4  10863  2addsub  10903  addsubeq4  10904  sub4  10934  muladd  11075  mulsub  11086  mulge0  11161  add20i  11186  mulge0i  11190  mulne0  11285  divmuldiv  11343  rec11i  11384  ltmul12a  11499  mulge0b  11513  zmulcl  12034  uz2mulcl  12329  qaddcl  12367  qmulcl  12369  qreccl  12371  rpaddcl  12414  xmulgt0  12679  xmulge0  12680  ixxin  12758  ge0addcl  12851  ge0xaddcl  12853  fzadd2  12945  serge0  13427  expge1  13469  sqrmo  14614  rexanuz  14708  amgm2  14732  bhmafibid1cn  14826  bhmafibid2cn  14827  mulcn2  14955  dvds2ln  15645  opoe  15715  omoe  15716  opeo  15717  omeo  15718  divalglem6  15752  divalglem8  15754  lcmcllem  15943  lcmgcd  15954  lcmdvds  15955  pc2dvds  16218  catpropd  16982  gimco  18411  efgrelexlemb  18879  pf1ind  20521  psgnghm  20727  tgcl  21580  innei  21736  iunconnlem  22038  txbas  22178  txss12  22216  txbasval  22217  tx1stc  22261  fbunfip  22480  tsmsxp  22766  blsscls2  23117  bddnghm  23338  qtopbaslem  23370  iimulcl  23544  icoopnst  23546  iocopnst  23547  iccpnfcnv  23551  mumullem2  25760  fsumvma  25792  lgslem3  25878  pntrsumbnd2  26146  ajmoi  28638  hvadd4  28816  hvsub4  28817  shsel3  29095  shscli  29097  shscom  29099  chj4  29315  5oalem3  29436  5oalem5  29438  5oalem6  29439  hoadd4  29564  adjmo  29612  adjsym  29613  cnvadj  29672  leopmuli  29913  mdslmd1lem2  30106  chirredlem2  30171  chirredi  30174  cdjreui  30212  addltmulALT  30226  reofld  30917  xrge0iifcnv  31180  poseq  33099  frr3g  33125  funtransport  33496  btwnconn1lem13  33564  btwnconn1lem14  33565  outsideofeu  33596  outsidele  33597  funray  33605  lineintmo  33622  bj-nnfan  34081  bj-nnfor  34083  icoreclin  34642  poimirlem27  34923  heicant  34931  itg2gt0cn  34951  bndss  35068  isdrngo3  35241  riscer  35270  intidl  35311  unxpwdom3  39701  gbegt5  43933