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  963  imain  5361  tfrlemisucaccv  6418  tfrexlem  6427  tfr1onlemsucaccv  6434  tfrcllemsucaccv  6447  eroveu  6720  addcmpblnq  7487  mulcmpblnq  7488  ordpipqqs  7494  nqnq0pi  7558  addcmpblnq0  7563  mulcmpblnq0  7564  prarloclemcalc  7622  prarloc  7623  nqpru  7672  mullocpr  7691  distrlem4prl  7704  distrlem4pru  7705  ltprordil  7709  ltexprlemm  7720  ltexprlemopu  7723  ltexprlemupu  7724  ltexprlemru  7732  cauappcvgprlemopl  7766  cauappcvgprlem2  7780  caucvgprlemopl  7789  caucvgprlem2  7800  caucvgprprlemexbt  7826  caucvgprprlem2  7830  suplocexprlemloc  7841  suplocexprlemub  7843  suplocexprlemlub  7844  addcmpblnr  7859  mulcmpblnrlemg  7860  mulcmpblnr  7861  prsrlem1  7862  ltsrprg  7867  axmulcl  7986  ltmul1  8672  divdivdivap  8793  divmuleqap  8797  divsubdivap  8808  lt2mul2div  8959  ledivdiv  8970  lediv12a  8974  ssfzo12bi  10361  suprzcl2dc  10389  exbtwnz  10400  qbtwnre  10406  ioom  10410  seq3caopr  10647  seqcaoprg  10648  leexp2r  10745  hashunlem  10956  recvguniq  11350  rsqrmo  11382  fsum2dlemstep  11789  expcnvre  11858  fprod2dlemstep  11977  bezout  12376  qredeu  12463  pw2dvdseu  12534  oddpwdclemdvds  12536  pcqmul  12670  pcadd  12707  pockthg  12724  grprida  13263  issubmd  13350  ghmpreima  13646  unitgrp  13922  lmodprop2d  14154  lsspropdg  14237  neiint  14661  restbasg  14684  iscnp4  14734  cnpnei  14735  cnptopco  14738  blssps  14943  blss  14944  metequiv2  15012  xmetxpbl  15024  suplociccex  15141  dedekindicc  15149  limcimolemlt  15180  lgsquad2lem2  15603  2sqlem5  15640