Theorem an4s 659

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  an42s  660  anandis  677  anandirs  678  ax13  2375  nfeqf  2381  frminex  5656  trin2  6122  funprg  6600  funcnvqp  6610  fnun  6661  2elresin  6669  f1cof1  6796  f1coOLD  6798  f1oun  6850  f1oco  6854  fvreseq0  7037  f1mpt  7257  poxp  8111  soxp  8112  poseq  8141  wfr3g  8304  wfrfunOLD  8316  tfrlem7  8380  oeoe  8596  brecop  8801  pmss12g  8860  dif1ennnALT  9274  fiin  9414  tcmin  9733  frr3g  9748  harval2  9989  genpv  10991  genpdm  10994  genpnnp  10997  genpcd  10998  genpnmax  10999  addcmpblnr  11061  ltsrpr  11069  addclsr  11075  mulclsr  11076  addasssr  11080  mulasssr  11082  distrsr  11083  mulgt0sr  11097  addresr  11130  mulresr  11131  axaddf  11137  axmulf  11138  axaddass  11148  axmulass  11149  axdistr  11150  mulgt0  11288  mul4  11379  add4  11431  2addsub  11471  addsubeq4  11472  sub4  11502  muladd  11643  mulsub  11654  mulge0  11729  add20i  11754  mulge0i  11758  mulne0  11853  divmuldiv  11911  rec11i  11952  ltmul12a  12067  mulge0b  12081  zmulcl  12608  uz2mulcl  12907  qaddcl  12946  qmulcl  12948  qreccl  12950  rpaddcl  12993  xmulgt0  13259  xmulge0  13260  ixxin  13338  ge0addcl  13434  ge0xaddcl  13436  fzadd2  13533  serge0  14019  expge1  14062  sqrmo  15195  rexanuz  15289  amgm2  15313  bhmafibid1cn  15407  bhmafibid2cn  15408  mulcn2  15537  dvds2ln  16229  opoe  16303  omoe  16304  opeo  16305  omeo  16306  divalglem6  16338  divalglem8  16340  lcmcllem  16530  lcmgcd  16541  lcmdvds  16542  pc2dvds  16809  catpropd  17650  gimco  19137  efgrelexlemb  19613  psgnghm  21125  pf1ind  21866  tgcl  22464  innei  22621  iunconnlem  22923  txbas  23063  txss12  23101  txbasval  23102  tx1stc  23146  fbunfip  23365  tsmsxp  23651  blsscls2  24005  bddnghm  24235  qtopbaslem  24267  iimulcl  24445  icoopnst  24447  iocopnst  24448  iccpnfcnv  24452  mumullem2  26674  fsumvma  26706  lgslem3  26792  pntrsumbnd2  27060  mulsuniflem  27594  ajmoi  30099  hvadd4  30277  hvsub4  30278  shsel3  30556  shscli  30558  shscom  30560  chj4  30776  5oalem3  30897  5oalem5  30899  5oalem6  30900  hoadd4  31025  adjmo  31073  adjsym  31074  cnvadj  31133  leopmuli  31374  mdslmd1lem2  31567  chirredlem2  31632  chirredi  31635  cdjreui  31673  addltmulALT  31687  reofld  32448  xrge0iifcnv  32902  funtransport  34992  btwnconn1lem13  35060  btwnconn1lem14  35061  outsideofeu  35092  outsidele  35093  funray  35101  lineintmo  35118  bj-nnfan  35615  bj-nnfor  35617  icoreclin  36227  poimirlem27  36504  heicant  36512  itg2gt0cn  36532  bndss  36643  isdrngo3  36816  riscer  36845  intidl  36886  rimco  41091  unxpwdom3  41823  gbegt5  46416