Theorem simprrl 528

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 108	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 482	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  dn1dc  944  imain  5205  grpridd  5967  tfrlemisucaccv  6222  tfrexlem  6231  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  eroveu  6520  addcmpblnq  7175  mulcmpblnq  7176  ordpipqqs  7182  nqnq0pi  7246  addcmpblnq0  7251  mulcmpblnq0  7252  prarloclemcalc  7310  prarloc  7311  nqpru  7360  mullocpr  7379  distrlem4prl  7392  distrlem4pru  7393  ltprordil  7397  ltexprlemm  7408  ltexprlemopu  7411  ltexprlemupu  7412  ltexprlemru  7420  cauappcvgprlemopl  7454  cauappcvgprlem2  7468  caucvgprlemopl  7477  caucvgprlem2  7488  caucvgprprlemexbt  7514  caucvgprprlem2  7518  suplocexprlemloc  7529  suplocexprlemub  7531  suplocexprlemlub  7532  addcmpblnr  7547  mulcmpblnrlemg  7548  mulcmpblnr  7549  prsrlem1  7550  ltsrprg  7555  axmulcl  7674  ltmul1  8354  divdivdivap  8473  divmuleqap  8477  divsubdivap  8488  lt2mul2div  8637  ledivdiv  8648  lediv12a  8652  ssfzo12bi  10002  exbtwnz  10028  qbtwnre  10034  ioom  10038  seq3caopr  10256  leexp2r  10347  hashunlem  10550  recvguniq  10767  rsqrmo  10799  fsum2dlemstep  11203  expcnvre  11272  bezout  11699  qredeu  11778  pw2dvdseu  11846  oddpwdclemdvds  11848  neiint  12314  restbasg  12337  iscnp4  12387  cnpnei  12388  cnptopco  12391  blssps  12596  blss  12597  metequiv2  12665  xmetxpbl  12677  suplociccex  12772  dedekindicc  12780  limcimolemlt  12802