Theorem simplrl 541

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrl	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 493	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  rmob  3145  disjiun  4125  f1imass  5980  riota5f  6065  tfrexlem  6605  tfrcl  6635  nnsucuniel  6768  nntr2  6776  pw2f1odclem  7134  fopwdom  7136  fidceq  7171  fisbth  7187  fidcen  7203  fientri3  7222  unsnfidcex  7227  undifdc  7231  iunfidisj  7260  fiuni  7312  2omap  7318  ordiso2  7375  nninfninc  7463  acfun  7563  2omotaplemap  7623  ccfunen  7630  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  addcmpblnq0  7810  mulcmpblnq0  7811  prml  7844  addlocpr  7903  prmuloc  7933  mullocpr  7938  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  aptiprleml  8006  ltmprr  8009  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemloc  8019  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemloc  8042  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  suplocexprlemrl  8084  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  ltsrprg  8114  mulgt0sr  8145  caucvgsrlemgt1  8162  suplocsrlemb  8173  axmulcl  8233  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  cnegexlem1  8501  negeu  8517  add20  8802  apreap  8916  cru  8931  apsym  8935  apcotr  8936  apadd1  8937  apneg  8940  mulext1  8941  mulge0  8948  mulap0  8983  divdivdivap  9044  prodgt0  9183  ltmul12a  9191  lt2mul2div  9210  ledivdiv  9221  lediv12a  9225  qapne  10041  xleadd1a  10277  ixxss12  10310  elfz0ubfz0  10534  qtri3or  10677  exbtwnzlemstep  10684  exbtwnzlemex  10686  exbtwnz  10687  rebtwn2zlemstep  10689  rebtwn2z  10691  btwnzge0  10737  iseqf1olemqf1o  10945  mulexpzap  11018  leexp1a  11033  hashen  11225  fihashdom  11245  hashun  11247  hashf1lem2  11288  swrdccatin1  11499  pfxccatin12lem3  11506  pfxccat3  11508  cjap  11674  cvg1nlemres  11753  rsqrmo  11795  abslt  11856  abs3lem  11879  cau3lem  11882  rexanre  11988  xrmaxltsup  12026  climcau  12115  sumeq2  12127  summodc  12152  fisumss  12161  fsum2d  12204  fsumabs  12234  fsumiun  12246  prodeq2  12326  prodmodclem2  12346  fprodcl2lem  12374  fprodap0  12390  fprod2d  12392  fprodrec  12398  fprodap0f  12405  fprodle  12409  eirrap  12547  divalglemeunn  12690  divalglemeuneg  12692  bezoutlemnewy  12775  bezoutlemstep  12776  bezoutlemmain  12777  bezoutlembi  12784  bezoutlemeu  12786  qredeu  12877  isprm5lem  12921  pw2dvdseu  12948  sqrt2irrap  12960  pythagtriplem2  13047  pythagtrip  13064  pclemub  13068  pcqmul  13084  pcexp  13090  pcneg  13106  pcprmpw2  13114  pcadd  13121  prmpwdvds  13136  4sqlem13m  13184  ballotfilemsf1o  13259  ennnfonelemg  13296  ennnfonelemrnh  13309  ctiunctlemfo  13332  nninfdclemf1  13345  imasival  13629  sgrppropd  13730  ismndd  13752  mndpropd  13755  mhmeql  13801  mhmmnd  13921  mulgfng  13929  issubg4m  13998  ssnmz  14016  conjnmzb  14085  gsumvalfi  14154  rngpropd  14256  ringpropd  14345  dvdsrtr  14410  aprlring  14602  islmod  14629  assapropd  15016  mplsubgfilemcl  15092  restbasg  15271  cnpnei  15322  cnptoprest2  15343  cnpdis  15345  lmtopcnp  15353  txcnp  15374  ismet2  15457  blininf  15527  metss2lem  15600  xmettxlem  15612  xmettx  15613  metcnp  15615  metcnpi3  15620  addcncntoplem  15664  fsumcncntop  15670  mulc1cncf  15692  cncfco  15694  mulcncf  15711  dedekindeulemuub  15720  dedekindeu  15726  dedekindicclemuub  15729  ivthinclemloc  15744  ivthinc  15746  limcimo  15768  limccnp2cntop  15780  dveflem  15829  plyf  15840  plyco  15862  plycj  15864  dvply2g  15869  logbgcd1irrap  16078  perfectlem2  16120  lgsdilem  16158  lgsquad2lem2  16213  lgsquad3  16215  2sqlem5  16250  2sqlem9  16255  usgredg4  16468  usgr1eop  16498  usgr1vr  16501  subuhgr  16525  subumgr  16527  subusgr  16528  clwwlknonex2lem2  16691  pw1map  17037  qdencn  17084  apdiff  17109  qdiff  17110