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  962  imain  5337  tfrlemisucaccv  6380  tfrexlem  6389  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  eroveu  6682  addcmpblnq  7429  mulcmpblnq  7430  ordpipqqs  7436  nqnq0pi  7500  addcmpblnq0  7505  mulcmpblnq0  7506  prarloclemcalc  7564  prarloc  7565  nqpru  7614  mullocpr  7633  distrlem4prl  7646  distrlem4pru  7647  ltprordil  7651  ltexprlemm  7662  ltexprlemopu  7665  ltexprlemupu  7666  ltexprlemru  7674  cauappcvgprlemopl  7708  cauappcvgprlem2  7722  caucvgprlemopl  7731  caucvgprlem2  7742  caucvgprprlemexbt  7768  caucvgprprlem2  7772  suplocexprlemloc  7783  suplocexprlemub  7785  suplocexprlemlub  7786  addcmpblnr  7801  mulcmpblnrlemg  7802  mulcmpblnr  7803  prsrlem1  7804  ltsrprg  7809  axmulcl  7928  ltmul1  8613  divdivdivap  8734  divmuleqap  8738  divsubdivap  8749  lt2mul2div  8900  ledivdiv  8911  lediv12a  8915  ssfzo12bi  10295  exbtwnz  10322  qbtwnre  10328  ioom  10332  seq3caopr  10569  seqcaoprg  10570  leexp2r  10667  hashunlem  10878  recvguniq  11142  rsqrmo  11174  fsum2dlemstep  11580  expcnvre  11649  fprod2dlemstep  11768  suprzcl2dc  12095  bezout  12151  qredeu  12238  pw2dvdseu  12309  oddpwdclemdvds  12311  pcqmul  12444  pcadd  12481  pockthg  12498  grprida  12973  issubmd  13049  ghmpreima  13339  unitgrp  13615  lmodprop2d  13847  lsspropdg  13930  neiint  14324  restbasg  14347  iscnp4  14397  cnpnei  14398  cnptopco  14401  blssps  14606  blss  14607  metequiv2  14675  xmetxpbl  14687  suplociccex  14804  dedekindicc  14812  limcimolemlt  14843  lgsquad2lem2  15239  2sqlem5  15276