Theorem simprrl 545

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 495	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  973  imain  5461  tfrlemisucaccv  6590  tfrexlem  6599  tfr1onlemsucaccv  6606  tfrcllemsucaccv  6619  eroveu  6894  addcmpblnq  7728  mulcmpblnq  7729  ordpipqqs  7735  nqnq0pi  7799  addcmpblnq0  7804  mulcmpblnq0  7805  prarloclemcalc  7863  prarloc  7864  nqpru  7913  mullocpr  7932  distrlem4prl  7945  distrlem4pru  7946  ltprordil  7950  ltexprlemm  7961  ltexprlemopu  7964  ltexprlemupu  7965  ltexprlemru  7973  cauappcvgprlemopl  8007  cauappcvgprlem2  8021  caucvgprlemopl  8030  caucvgprlem2  8041  caucvgprprlemexbt  8067  caucvgprprlem2  8071  suplocexprlemloc  8082  suplocexprlemub  8084  suplocexprlemlub  8085  addcmpblnr  8100  mulcmpblnrlemg  8101  mulcmpblnr  8102  prsrlem1  8103  ltsrprg  8108  axmulcl  8227  ltmul1  8914  divdivdivap  9037  divmuleqap  9041  divsubdivap  9052  lt2mul2div  9203  ledivdiv  9214  lediv12a  9218  ssfzo12bi  10626  infssfzcldc  10652  infssfzledc  10653  suprzcl2dc  10657  exbtwnz  10668  qbtwnre  10674  ioom  10678  seq3caopr  10915  seqcaoprg  10916  leexp2r  11013  hashunlem  11227  hashfibclem  11265  wrd2ind  11478  recvguniq  11744  rsqrmo  11776  fsum2dlemstep  12184  expcnvre  12253  fprod2dlemstep  12372  bezout  12771  qredeu  12858  pw2dvdseu  12929  oddpwdclemdvds  12931  pcqmul  13065  pcadd  13102  pockthg  13119  grprida  13690  issubmd  13764  ghmpreima  14052  unitgrp  14406  lmodprop2d  14668  lsspropdg  14751  assapropd  14997  neiint  15229  restbasg  15252  iscnp4  15302  cnpnei  15303  cnptopco  15306  blssps  15511  blss  15512  metequiv2  15580  xmetxpbl  15592  suplociccex  15709  dedekindicc  15717  limcimolemlt  15748  pellexlem3  16076  lgsquad2lem2  16184  2sqlem5  16221