Theorem simprrl 541

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  969  imain  5437  tfrlemisucaccv  6555  tfrexlem  6564  tfr1onlemsucaccv  6571  tfrcllemsucaccv  6584  eroveu  6859  addcmpblnq  7678  mulcmpblnq  7679  ordpipqqs  7685  nqnq0pi  7749  addcmpblnq0  7754  mulcmpblnq0  7755  prarloclemcalc  7813  prarloc  7814  nqpru  7863  mullocpr  7882  distrlem4prl  7895  distrlem4pru  7896  ltprordil  7900  ltexprlemm  7911  ltexprlemopu  7914  ltexprlemupu  7915  ltexprlemru  7923  cauappcvgprlemopl  7957  cauappcvgprlem2  7971  caucvgprlemopl  7980  caucvgprlem2  7991  caucvgprprlemexbt  8017  caucvgprprlem2  8021  suplocexprlemloc  8032  suplocexprlemub  8034  suplocexprlemlub  8035  addcmpblnr  8050  mulcmpblnrlemg  8051  mulcmpblnr  8052  prsrlem1  8053  ltsrprg  8058  axmulcl  8177  ltmul1  8862  divdivdivap  8983  divmuleqap  8987  divsubdivap  8998  lt2mul2div  9149  ledivdiv  9160  lediv12a  9164  ssfzo12bi  10566  suprzcl2dc  10595  exbtwnz  10606  qbtwnre  10612  ioom  10616  seq3caopr  10853  seqcaoprg  10854  leexp2r  10951  hashunlem  11163  hashfibclem  11199  wrd2ind  11408  recvguniq  11673  rsqrmo  11705  fsum2dlemstep  12113  expcnvre  12182  fprod2dlemstep  12301  bezout  12700  qredeu  12787  pw2dvdseu  12858  oddpwdclemdvds  12860  pcqmul  12994  pcadd  13031  pockthg  13048  grprida  13589  issubmd  13676  ghmpreima  13972  unitgrp  14250  lmodprop2d  14483  lsspropdg  14566  neiint  14997  restbasg  15020  iscnp4  15070  cnpnei  15071  cnptopco  15074  blssps  15279  blss  15280  metequiv2  15348  xmetxpbl  15360  suplociccex  15477  dedekindicc  15485  limcimolemlt  15516  pellexlem3  15834  lgsquad2lem2  15942  2sqlem5  15979