Theorem simplrl 507

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  rmob  2969  disjiun  3890  f1imass  5629  riota5f  5708  tfrexlem  6185  tfrcl  6215  nnsucuniel  6345  nntr2  6353  fopwdom  6683  fidceq  6716  fisbth  6730  fientri3  6756  unsnfidcex  6761  undifdc  6765  iunfidisj  6786  fiuni  6818  ordiso2  6872  acfun  7011  ccfunen  7027  addcmpblnq  7123  mulcmpblnq  7124  ordpipqqs  7130  addcmpblnq0  7199  mulcmpblnq0  7200  prml  7233  addlocpr  7292  prmuloc  7322  mullocpr  7327  ltexprlemopl  7357  ltexprlemopu  7359  ltexprlemloc  7363  ltexprlemrl  7366  ltexprlemru  7368  addcanprleml  7370  addcanprlemu  7371  aptiprleml  7395  ltmprr  7398  cauappcvgprlemopl  7402  cauappcvgprlemopu  7404  cauappcvgprlemloc  7408  caucvgprlemopl  7425  caucvgprlemopu  7427  caucvgprlemloc  7431  caucvgprprlemopu  7455  caucvgprprlemloc  7459  caucvgprprlemexbt  7462  caucvgprprlemaddq  7464  addcmpblnr  7482  mulcmpblnrlemg  7483  mulcmpblnr  7484  ltsrprg  7490  mulgt0sr  7520  caucvgsrlemgt1  7537  axmulcl  7601  axcaucvglemres  7634  cnegexlem1  7860  negeu  7876  add20  8155  apreap  8267  cru  8282  apsym  8286  apcotr  8287  apadd1  8288  apneg  8291  mulext1  8292  mulge0  8299  mulap0  8328  divdivdivap  8386  prodgt0  8520  ltmul12a  8528  lt2mul2div  8547  ledivdiv  8558  lediv12a  8562  qapne  9333  xleadd1a  9549  ixxss12  9582  elfz0ubfz0  9795  qtri3or  9913  exbtwnzlemstep  9918  exbtwnzlemex  9920  exbtwnz  9921  rebtwn2zlemstep  9923  rebtwn2z  9925  btwnzge0  9966  iseqf1olemqf1o  10159  mulexpzap  10226  leexp1a  10241  hashen  10423  fihashdom  10442  hashun  10444  cjap  10571  cvg1nlemres  10649  rsqrmo  10691  abslt  10752  abs3lem  10775  cau3lem  10778  rexanre  10884  xrmaxltsup  10919  climcau  11008  sumeq2  11020  summodc  11044  fisumss  11053  fsum2d  11096  fsumabs  11126  fsumiun  11138  eirrap  11332  divalglemeunn  11466  divalglemeuneg  11468  bezoutlemnewy  11530  bezoutlemstep  11531  bezoutlemmain  11532  bezoutlembi  11539  bezoutlemeu  11541  qredeu  11624  pw2dvdseu  11691  sqrt2irrap  11703  ennnfonelemg  11761  ennnfonelemrnh  11774  ctiunctlemfo  11795  restbasg  12180  cnpnei  12230  cnptoprest2  12251  cnpdis  12253  lmtopcnp  12261  txcnp  12282  ismet2  12343  blininf  12413  metss2lem  12486  xmettxlem  12498  xmettx  12499  metcnp  12501  metcnpi3  12506  addcncntoplem  12537  fsumcncntop  12542  mulc1cncf  12562  cncfco  12564  mulcncf  12577  limcimo  12590  limccnp2cntop  12602  qdencn  12912