Theorem simprrl 545

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 495	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  dn1dc  973  imain  5466  tfrlemisucaccv  6600  tfrexlem  6609  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  eroveu  6904  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  nqnq0pi  7812  addcmpblnq0  7817  mulcmpblnq0  7818  prarloclemcalc  7876  prarloc  7877  nqpru  7926  mullocpr  7945  distrlem4prl  7958  distrlem4pru  7959  ltprordil  7963  ltexprlemm  7974  ltexprlemopu  7977  ltexprlemupu  7978  ltexprlemru  7986  cauappcvgprlemopl  8020  cauappcvgprlem2  8034  caucvgprlemopl  8043  caucvgprlem2  8054  caucvgprprlemexbt  8080  caucvgprprlem2  8084  suplocexprlemloc  8095  suplocexprlemub  8097  suplocexprlemlub  8098  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  prsrlem1  8116  ltsrprg  8121  axmulcl  8240  ltmul1  8929  divdivdivap  9052  divmuleqap  9056  divsubdivap  9067  lt2mul2div  9218  ledivdiv  9229  lediv12a  9233  ssfzo12bi  10661  infssfzcldc  10687  infssfzledc  10688  suprzcl2dc  10692  exbtwnz  10703  qbtwnre  10709  ioom  10713  seq3caopr  10954  seqcaoprg  10955  leexp2r  11052  hashunlem  11267  hashfibclem  11305  wrd2ind  11518  recvguniq  11784  rsqrmo  11816  fsum2dlemstep  12227  expcnvre  12296  fprod2dlemstep  12415  bezout  12814  qredeu  12901  pwbdvdseu  12973  nnmaxpwlemdvds  12975  nnmaxpwlemparts  12978  pcqmul  13112  pcadd  13149  pockthg  13166  grprida  13767  issubmd  13841  ghmpreima  14129  gsum2d2fi  14275  unitgrp  14533  lmodprop2d  14795  lsspropdg  14878  assapropd  15124  neiint  15383  restbasg  15406  iscnp4  15456  cnpnei  15457  cnptopco  15460  blssps  15665  blss  15666  metequiv2  15734  xmetxpbl  15746  suplociccex  15863  dedekindicc  15871  limcimolemlt  15902  pellexlem3  16243  lgsquad2lem2  16418  2sqlem5  16455