Theorem simprrl 541

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  968  imain  5412  tfrlemisucaccv  6491  tfrexlem  6500  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  eroveu  6795  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  nqnq0pi  7658  addcmpblnq0  7663  mulcmpblnq0  7664  prarloclemcalc  7722  prarloc  7723  nqpru  7772  mullocpr  7791  distrlem4prl  7804  distrlem4pru  7805  ltprordil  7809  ltexprlemm  7820  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemru  7832  cauappcvgprlemopl  7866  cauappcvgprlem2  7880  caucvgprlemopl  7889  caucvgprlem2  7900  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  prsrlem1  7962  ltsrprg  7967  axmulcl  8086  ltmul1  8772  divdivdivap  8893  divmuleqap  8897  divsubdivap  8908  lt2mul2div  9059  ledivdiv  9070  lediv12a  9074  ssfzo12bi  10471  suprzcl2dc  10500  exbtwnz  10511  qbtwnre  10517  ioom  10521  seq3caopr  10758  seqcaoprg  10759  leexp2r  10856  hashunlem  11068  wrd2ind  11305  recvguniq  11557  rsqrmo  11589  fsum2dlemstep  11997  expcnvre  12066  fprod2dlemstep  12185  bezout  12584  qredeu  12671  pw2dvdseu  12742  oddpwdclemdvds  12744  pcqmul  12878  pcadd  12915  pockthg  12932  grprida  13472  issubmd  13559  ghmpreima  13855  unitgrp  14133  lmodprop2d  14365  lsspropdg  14448  neiint  14872  restbasg  14895  iscnp4  14945  cnpnei  14946  cnptopco  14949  blssps  15154  blss  15155  metequiv2  15223  xmetxpbl  15235  suplociccex  15352  dedekindicc  15360  limcimolemlt  15391  lgsquad2lem2  15814  2sqlem5  15851