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  966  imain  5403  tfrlemisucaccv  6477  tfrexlem  6486  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  eroveu  6781  addcmpblnq  7562  mulcmpblnq  7563  ordpipqqs  7569  nqnq0pi  7633  addcmpblnq0  7638  mulcmpblnq0  7639  prarloclemcalc  7697  prarloc  7698  nqpru  7747  mullocpr  7766  distrlem4prl  7779  distrlem4pru  7780  ltprordil  7784  ltexprlemm  7795  ltexprlemopu  7798  ltexprlemupu  7799  ltexprlemru  7807  cauappcvgprlemopl  7841  cauappcvgprlem2  7855  caucvgprlemopl  7864  caucvgprlem2  7875  caucvgprprlemexbt  7901  caucvgprprlem2  7905  suplocexprlemloc  7916  suplocexprlemub  7918  suplocexprlemlub  7919  addcmpblnr  7934  mulcmpblnrlemg  7935  mulcmpblnr  7936  prsrlem1  7937  ltsrprg  7942  axmulcl  8061  ltmul1  8747  divdivdivap  8868  divmuleqap  8872  divsubdivap  8883  lt2mul2div  9034  ledivdiv  9045  lediv12a  9049  ssfzo12bi  10439  suprzcl2dc  10467  exbtwnz  10478  qbtwnre  10484  ioom  10488  seq3caopr  10725  seqcaoprg  10726  leexp2r  10823  hashunlem  11034  wrd2ind  11263  recvguniq  11514  rsqrmo  11546  fsum2dlemstep  11953  expcnvre  12022  fprod2dlemstep  12141  bezout  12540  qredeu  12627  pw2dvdseu  12698  oddpwdclemdvds  12700  pcqmul  12834  pcadd  12871  pockthg  12888  grprida  13428  issubmd  13515  ghmpreima  13811  unitgrp  14088  lmodprop2d  14320  lsspropdg  14403  neiint  14827  restbasg  14850  iscnp4  14900  cnpnei  14901  cnptopco  14904  blssps  15109  blss  15110  metequiv2  15178  xmetxpbl  15190  suplociccex  15307  dedekindicc  15315  limcimolemlt  15346  lgsquad2lem2  15769  2sqlem5  15806