Theorem simprrl 539

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

Assertion

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

Proof of Theorem simprrl

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 491	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:  dn1dc  961  imain  5310  tfrlemisucaccv  6340  tfrexlem  6349  tfr1onlemsucaccv  6356  tfrcllemsucaccv  6369  eroveu  6640  addcmpblnq  7380  mulcmpblnq  7381  ordpipqqs  7387  nqnq0pi  7451  addcmpblnq0  7456  mulcmpblnq0  7457  prarloclemcalc  7515  prarloc  7516  nqpru  7565  mullocpr  7584  distrlem4prl  7597  distrlem4pru  7598  ltprordil  7602  ltexprlemm  7613  ltexprlemopu  7616  ltexprlemupu  7617  ltexprlemru  7625  cauappcvgprlemopl  7659  cauappcvgprlem2  7673  caucvgprlemopl  7682  caucvgprlem2  7693  caucvgprprlemexbt  7719  caucvgprprlem2  7723  suplocexprlemloc  7734  suplocexprlemub  7736  suplocexprlemlub  7737  addcmpblnr  7752  mulcmpblnrlemg  7753  mulcmpblnr  7754  prsrlem1  7755  ltsrprg  7760  axmulcl  7879  ltmul1  8563  divdivdivap  8684  divmuleqap  8688  divsubdivap  8699  lt2mul2div  8850  ledivdiv  8861  lediv12a  8865  ssfzo12bi  10239  exbtwnz  10265  qbtwnre  10271  ioom  10275  seq3caopr  10497  leexp2r  10588  hashunlem  10798  recvguniq  11018  rsqrmo  11050  fsum2dlemstep  11456  expcnvre  11525  fprod2dlemstep  11644  suprzcl2dc  11970  bezout  12026  qredeu  12111  pw2dvdseu  12182  oddpwdclemdvds  12184  pcqmul  12317  pcadd  12353  pockthg  12369  grprida  12825  issubmd  12887  unitgrp  13364  lmodprop2d  13537  lsspropdg  13620  neiint  13941  restbasg  13964  iscnp4  14014  cnpnei  14015  cnptopco  14018  blssps  14223  blss  14224  metequiv2  14292  xmetxpbl  14304  suplociccex  14399  dedekindicc  14407  limcimolemlt  14429  2sqlem5  14762