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  960  imain  5299  tfrlemisucaccv  6326  tfrexlem  6335  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  eroveu  6626  addcmpblnq  7366  mulcmpblnq  7367  ordpipqqs  7373  nqnq0pi  7437  addcmpblnq0  7442  mulcmpblnq0  7443  prarloclemcalc  7501  prarloc  7502  nqpru  7551  mullocpr  7570  distrlem4prl  7583  distrlem4pru  7584  ltprordil  7588  ltexprlemm  7599  ltexprlemopu  7602  ltexprlemupu  7603  ltexprlemru  7611  cauappcvgprlemopl  7645  cauappcvgprlem2  7659  caucvgprlemopl  7668  caucvgprlem2  7679  caucvgprprlemexbt  7705  caucvgprprlem2  7709  suplocexprlemloc  7720  suplocexprlemub  7722  suplocexprlemlub  7723  addcmpblnr  7738  mulcmpblnrlemg  7739  mulcmpblnr  7740  prsrlem1  7741  ltsrprg  7746  axmulcl  7865  ltmul1  8549  divdivdivap  8670  divmuleqap  8674  divsubdivap  8685  lt2mul2div  8836  ledivdiv  8847  lediv12a  8851  ssfzo12bi  10225  exbtwnz  10251  qbtwnre  10257  ioom  10261  seq3caopr  10483  leexp2r  10574  hashunlem  10784  recvguniq  11004  rsqrmo  11036  fsum2dlemstep  11442  expcnvre  11511  fprod2dlemstep  11630  suprzcl2dc  11956  bezout  12012  qredeu  12097  pw2dvdseu  12168  oddpwdclemdvds  12170  pcqmul  12303  pcadd  12339  pockthg  12355  grpridd  12806  issubmd  12865  unitgrp  13285  lmodprop2d  13438  neiint  13648  restbasg  13671  iscnp4  13721  cnpnei  13722  cnptopco  13725  blssps  13930  blss  13931  metequiv2  13999  xmetxpbl  14011  suplociccex  14106  dedekindicc  14114  limcimolemlt  14136  2sqlem5  14469