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  965  imain  5379  tfrlemisucaccv  6441  tfrexlem  6450  tfr1onlemsucaccv  6457  tfrcllemsucaccv  6470  eroveu  6743  addcmpblnq  7522  mulcmpblnq  7523  ordpipqqs  7529  nqnq0pi  7593  addcmpblnq0  7598  mulcmpblnq0  7599  prarloclemcalc  7657  prarloc  7658  nqpru  7707  mullocpr  7726  distrlem4prl  7739  distrlem4pru  7740  ltprordil  7744  ltexprlemm  7755  ltexprlemopu  7758  ltexprlemupu  7759  ltexprlemru  7767  cauappcvgprlemopl  7801  cauappcvgprlem2  7815  caucvgprlemopl  7824  caucvgprlem2  7835  caucvgprprlemexbt  7861  caucvgprprlem2  7865  suplocexprlemloc  7876  suplocexprlemub  7878  suplocexprlemlub  7879  addcmpblnr  7894  mulcmpblnrlemg  7895  mulcmpblnr  7896  prsrlem1  7897  ltsrprg  7902  axmulcl  8021  ltmul1  8707  divdivdivap  8828  divmuleqap  8832  divsubdivap  8843  lt2mul2div  8994  ledivdiv  9005  lediv12a  9009  ssfzo12bi  10398  suprzcl2dc  10426  exbtwnz  10437  qbtwnre  10443  ioom  10447  seq3caopr  10684  seqcaoprg  10685  leexp2r  10782  hashunlem  10993  wrd2ind  11221  recvguniq  11472  rsqrmo  11504  fsum2dlemstep  11911  expcnvre  11980  fprod2dlemstep  12099  bezout  12498  qredeu  12585  pw2dvdseu  12656  oddpwdclemdvds  12658  pcqmul  12792  pcadd  12829  pockthg  12846  grprida  13386  issubmd  13473  ghmpreima  13769  unitgrp  14045  lmodprop2d  14277  lsspropdg  14360  neiint  14784  restbasg  14807  iscnp4  14857  cnpnei  14858  cnptopco  14861  blssps  15066  blss  15067  metequiv2  15135  xmetxpbl  15147  suplociccex  15264  dedekindicc  15272  limcimolemlt  15303  lgsquad2lem2  15726  2sqlem5  15763