Theorem simplrl 524

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 480	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  2996  disjiun  3919  f1imass  5668  riota5f  5747  tfrexlem  6224  tfrcl  6254  nnsucuniel  6384  nntr2  6392  fopwdom  6723  fidceq  6756  fisbth  6770  fientri3  6796  unsnfidcex  6801  undifdc  6805  iunfidisj  6827  fiuni  6859  ordiso2  6913  acfun  7056  ccfunen  7072  addcmpblnq  7168  mulcmpblnq  7169  ordpipqqs  7175  addcmpblnq0  7244  mulcmpblnq0  7245  prml  7278  addlocpr  7337  prmuloc  7367  mullocpr  7372  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemloc  7408  ltexprlemrl  7411  ltexprlemru  7413  addcanprleml  7415  addcanprlemu  7416  aptiprleml  7440  ltmprr  7443  cauappcvgprlemopl  7447  cauappcvgprlemopu  7449  cauappcvgprlemloc  7453  caucvgprlemopl  7470  caucvgprlemopu  7472  caucvgprlemloc  7476  caucvgprprlemopu  7500  caucvgprprlemloc  7504  caucvgprprlemexbt  7507  caucvgprprlemaddq  7509  suplocexprlemrl  7518  suplocexprlemdisj  7521  suplocexprlemloc  7522  suplocexprlemub  7524  addcmpblnr  7540  mulcmpblnrlemg  7541  mulcmpblnr  7542  ltsrprg  7548  mulgt0sr  7579  caucvgsrlemgt1  7596  suplocsrlemb  7607  axmulcl  7667  axcaucvglemres  7700  axpre-suploclemres  7702  axpre-suploc  7703  cnegexlem1  7930  negeu  7946  add20  8229  apreap  8342  cru  8357  apsym  8361  apcotr  8362  apadd1  8363  apneg  8366  mulext1  8367  mulge0  8374  mulap0  8408  divdivdivap  8466  prodgt0  8603  ltmul12a  8611  lt2mul2div  8630  ledivdiv  8641  lediv12a  8645  qapne  9424  xleadd1a  9649  ixxss12  9682  elfz0ubfz0  9895  qtri3or  10013  exbtwnzlemstep  10018  exbtwnzlemex  10020  exbtwnz  10021  rebtwn2zlemstep  10023  rebtwn2z  10025  btwnzge0  10066  iseqf1olemqf1o  10259  mulexpzap  10326  leexp1a  10341  hashen  10523  fihashdom  10542  hashun  10544  cjap  10671  cvg1nlemres  10750  rsqrmo  10792  abslt  10853  abs3lem  10876  cau3lem  10879  rexanre  10985  xrmaxltsup  11020  climcau  11109  sumeq2  11121  summodc  11145  fisumss  11154  fsum2d  11197  fsumabs  11227  fsumiun  11239  prodeq2  11319  eirrap  11473  divalglemeunn  11607  divalglemeuneg  11609  bezoutlemnewy  11673  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlembi  11682  bezoutlemeu  11684  qredeu  11767  pw2dvdseu  11835  sqrt2irrap  11847  ennnfonelemg  11905  ennnfonelemrnh  11918  ctiunctlemfo  11941  restbasg  12326  cnpnei  12377  cnptoprest2  12398  cnpdis  12400  lmtopcnp  12408  txcnp  12429  ismet2  12512  blininf  12582  metss2lem  12655  xmettxlem  12667  xmettx  12668  metcnp  12670  metcnpi3  12675  addcncntoplem  12709  fsumcncntop  12714  mulc1cncf  12734  cncfco  12736  mulcncf  12749  dedekindeulemuub  12753  dedekindeu  12759  dedekindicclemuub  12762  ivthinclemloc  12777  ivthinc  12779  limcimo  12792  limccnp2cntop  12804  dveflem  12844  qdencn  13211