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  5463  tfrlemisucaccv  6596  tfrexlem  6605  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  eroveu  6900  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  nqnq0pi  7805  addcmpblnq0  7810  mulcmpblnq0  7811  prarloclemcalc  7869  prarloc  7870  nqpru  7919  mullocpr  7938  distrlem4prl  7951  distrlem4pru  7952  ltprordil  7956  ltexprlemm  7967  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemru  7979  cauappcvgprlemopl  8013  cauappcvgprlem2  8027  caucvgprlemopl  8036  caucvgprlem2  8047  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  prsrlem1  8109  ltsrprg  8114  axmulcl  8233  ltmul1  8921  divdivdivap  9044  divmuleqap  9048  divsubdivap  9059  lt2mul2div  9210  ledivdiv  9221  lediv12a  9225  ssfzo12bi  10645  infssfzcldc  10671  infssfzledc  10672  suprzcl2dc  10676  exbtwnz  10687  qbtwnre  10693  ioom  10697  seq3caopr  10934  seqcaoprg  10935  leexp2r  11032  hashunlem  11246  hashfibclem  11284  wrd2ind  11497  recvguniq  11763  rsqrmo  11795  fsum2dlemstep  12203  expcnvre  12272  fprod2dlemstep  12391  bezout  12790  qredeu  12877  pw2dvdseu  12948  oddpwdclemdvds  12950  pcqmul  13084  pcadd  13121  pockthg  13138  grprida  13709  issubmd  13783  ghmpreima  14071  unitgrp  14425  lmodprop2d  14687  lsspropdg  14770  assapropd  15016  neiint  15248  restbasg  15271  iscnp4  15321  cnpnei  15322  cnptopco  15325  blssps  15530  blss  15531  metequiv2  15599  xmetxpbl  15611  suplociccex  15728  dedekindicc  15736  limcimolemlt  15767  pellexlem3  16099  lgsquad2lem2  16213  2sqlem5  16250