Theorem simplrl 525

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 108	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 481	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  rmob  3038  disjiun  3971  f1imass  5736  riota5f  5816  tfrexlem  6293  tfrcl  6323  nnsucuniel  6454  nntr2  6462  fopwdom  6793  fidceq  6826  fisbth  6840  fientri3  6871  unsnfidcex  6876  undifdc  6880  iunfidisj  6902  fiuni  6934  ordiso2  6991  acfun  7154  ccfunen  7196  addcmpblnq  7299  mulcmpblnq  7300  ordpipqqs  7306  addcmpblnq0  7375  mulcmpblnq0  7376  prml  7409  addlocpr  7468  prmuloc  7498  mullocpr  7503  ltexprlemopl  7533  ltexprlemopu  7535  ltexprlemloc  7539  ltexprlemrl  7542  ltexprlemru  7544  addcanprleml  7546  addcanprlemu  7547  aptiprleml  7571  ltmprr  7574  cauappcvgprlemopl  7578  cauappcvgprlemopu  7580  cauappcvgprlemloc  7584  caucvgprlemopl  7601  caucvgprlemopu  7603  caucvgprlemloc  7607  caucvgprprlemopu  7631  caucvgprprlemloc  7635  caucvgprprlemexbt  7638  caucvgprprlemaddq  7640  suplocexprlemrl  7649  suplocexprlemdisj  7652  suplocexprlemloc  7653  suplocexprlemub  7655  addcmpblnr  7671  mulcmpblnrlemg  7672  mulcmpblnr  7673  ltsrprg  7679  mulgt0sr  7710  caucvgsrlemgt1  7727  suplocsrlemb  7738  axmulcl  7798  axcaucvglemres  7831  axpre-suploclemres  7833  axpre-suploc  7834  cnegexlem1  8064  negeu  8080  add20  8363  apreap  8476  cru  8491  apsym  8495  apcotr  8496  apadd1  8497  apneg  8500  mulext1  8501  mulge0  8508  mulap0  8542  divdivdivap  8600  prodgt0  8738  ltmul12a  8746  lt2mul2div  8765  ledivdiv  8776  lediv12a  8780  qapne  9568  xleadd1a  9800  ixxss12  9833  elfz0ubfz0  10050  qtri3or  10168  exbtwnzlemstep  10173  exbtwnzlemex  10175  exbtwnz  10176  rebtwn2zlemstep  10178  rebtwn2z  10180  btwnzge0  10225  iseqf1olemqf1o  10418  mulexpzap  10485  leexp1a  10500  hashen  10686  fihashdom  10705  hashun  10707  cjap  10834  cvg1nlemres  10913  rsqrmo  10955  abslt  11016  abs3lem  11039  cau3lem  11042  rexanre  11148  xrmaxltsup  11185  climcau  11274  sumeq2  11286  summodc  11310  fisumss  11319  fsum2d  11362  fsumabs  11392  fsumiun  11404  prodeq2  11484  prodmodclem2  11504  fprodcl2lem  11532  fprodap0  11548  fprod2d  11550  fprodrec  11556  fprodap0f  11563  fprodle  11567  eirrap  11704  divalglemeunn  11843  divalglemeuneg  11845  bezoutlemnewy  11914  bezoutlemstep  11915  bezoutlemmain  11916  bezoutlembi  11923  bezoutlemeu  11925  qredeu  12008  pw2dvdseu  12077  sqrt2irrap  12089  pythagtriplem2  12175  pythagtrip  12192  pclemub  12196  pcqmul  12212  pcexp  12218  pcneg  12233  pcprmpw2  12241  pcadd  12248  ennnfonelemg  12273  ennnfonelemrnh  12286  ctiunctlemfo  12309  nninfdclemf1  12324  restbasg  12709  cnpnei  12760  cnptoprest2  12781  cnpdis  12783  lmtopcnp  12791  txcnp  12812  ismet2  12895  blininf  12965  metss2lem  13038  xmettxlem  13050  xmettx  13051  metcnp  13053  metcnpi3  13058  addcncntoplem  13092  fsumcncntop  13097  mulc1cncf  13117  cncfco  13119  mulcncf  13132  dedekindeulemuub  13136  dedekindeu  13142  dedekindicclemuub  13145  ivthinclemloc  13160  ivthinc  13162  limcimo  13175  limccnp2cntop  13187  dveflem  13228  logbgcd1irrap  13429  qdencn  13740  apdiff  13761