Theorem simplrl 535

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 489	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  rmob  3055  disjiun  3998  f1imass  5774  riota5f  5854  tfrexlem  6334  tfrcl  6364  nnsucuniel  6495  nntr2  6503  fopwdom  6835  fidceq  6868  fisbth  6882  fientri3  6913  unsnfidcex  6918  undifdc  6922  iunfidisj  6944  fiuni  6976  ordiso2  7033  acfun  7205  2omotaplemap  7255  ccfunen  7262  addcmpblnq  7365  mulcmpblnq  7366  ordpipqqs  7372  addcmpblnq0  7441  mulcmpblnq0  7442  prml  7475  addlocpr  7534  prmuloc  7564  mullocpr  7569  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemloc  7605  ltexprlemrl  7608  ltexprlemru  7610  addcanprleml  7612  addcanprlemu  7613  aptiprleml  7637  ltmprr  7640  cauappcvgprlemopl  7644  cauappcvgprlemopu  7646  cauappcvgprlemloc  7650  caucvgprlemopl  7667  caucvgprlemopu  7669  caucvgprlemloc  7673  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemexbt  7704  caucvgprprlemaddq  7706  suplocexprlemrl  7715  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemub  7721  addcmpblnr  7737  mulcmpblnrlemg  7738  mulcmpblnr  7739  ltsrprg  7745  mulgt0sr  7776  caucvgsrlemgt1  7793  suplocsrlemb  7804  axmulcl  7864  axcaucvglemres  7897  axpre-suploclemres  7899  axpre-suploc  7900  cnegexlem1  8131  negeu  8147  add20  8430  apreap  8543  cru  8558  apsym  8562  apcotr  8563  apadd1  8564  apneg  8567  mulext1  8568  mulge0  8575  mulap0  8610  divdivdivap  8669  prodgt0  8808  ltmul12a  8816  lt2mul2div  8835  ledivdiv  8846  lediv12a  8850  qapne  9638  xleadd1a  9872  ixxss12  9905  elfz0ubfz0  10124  qtri3or  10242  exbtwnzlemstep  10247  exbtwnzlemex  10249  exbtwnz  10250  rebtwn2zlemstep  10252  rebtwn2z  10254  btwnzge0  10299  iseqf1olemqf1o  10492  mulexpzap  10559  leexp1a  10574  hashen  10763  fihashdom  10782  hashun  10784  cjap  10914  cvg1nlemres  10993  rsqrmo  11035  abslt  11096  abs3lem  11119  cau3lem  11122  rexanre  11228  xrmaxltsup  11265  climcau  11354  sumeq2  11366  summodc  11390  fisumss  11399  fsum2d  11442  fsumabs  11472  fsumiun  11484  prodeq2  11564  prodmodclem2  11584  fprodcl2lem  11612  fprodap0  11628  fprod2d  11630  fprodrec  11636  fprodap0f  11643  fprodle  11647  eirrap  11784  divalglemeunn  11925  divalglemeuneg  11927  bezoutlemnewy  11996  bezoutlemstep  11997  bezoutlemmain  11998  bezoutlembi  12005  bezoutlemeu  12007  qredeu  12096  isprm5lem  12140  pw2dvdseu  12167  sqrt2irrap  12179  pythagtriplem2  12265  pythagtrip  12282  pclemub  12286  pcqmul  12302  pcexp  12308  pcneg  12323  pcprmpw2  12331  pcadd  12338  prmpwdvds  12352  ennnfonelemg  12403  ennnfonelemrnh  12416  ctiunctlemfo  12439  nninfdclemf1  12452  imasival  12726  ismndd  12837  mndpropd  12840  mhmeql  12875  mhmmnd  12979  mulgfng  12986  issubg4m  13051  ssnmz  13069  ringpropd  13215  dvdsrtr  13268  islmod  13379  restbasg  13638  cnpnei  13689  cnptoprest2  13710  cnpdis  13712  lmtopcnp  13720  txcnp  13741  ismet2  13824  blininf  13894  metss2lem  13967  xmettxlem  13979  xmettx  13980  metcnp  13982  metcnpi3  13987  addcncntoplem  14021  fsumcncntop  14026  mulc1cncf  14046  cncfco  14048  mulcncf  14061  dedekindeulemuub  14065  dedekindeu  14071  dedekindicclemuub  14074  ivthinclemloc  14089  ivthinc  14091  limcimo  14104  limccnp2cntop  14116  dveflem  14157  logbgcd1irrap  14358  lgsdilem  14398  2sqlem5  14436  2sqlem9  14441  qdencn  14745  apdiff  14766