Theorem simprlr 544

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprlr	⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Proof of Theorem simprlr

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 494	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:  imain  5466  fcof1  5992  fliftfun  6005  sbthlemi6  7285  sbthlemi8  7287  suppeqfsuppbi  7301  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  enq0tr  7808  addcmpblnq0  7817  mulcmpblnq0  7818  nnnq0lem1  7820  addnq0mo  7821  mulnq0mo  7822  prarloclemcalc  7876  addlocpr  7910  distrlem4prl  7958  distrlem4pru  7959  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  prsrlem1  8116  addsrmo  8117  mulsrmo  8118  ltsrprg  8121  apreap  8924  apreim  8940  aptap  8987  divdivdivap  9052  divsubdivap  9067  ledivdiv  9229  lediv12a  9233  exbtwnz  10703  seq3caopr  10954  seqcaoprg  10955  leexp2r  11052  hashfibclem  11305  hashf1lem1  11308  hashf1lem2  11309  zfz1iso  11316  wrd2ind  11518  swrdccat  11530  recvguniq  11784  rsqrmo  11816  summodclem2  12175  prodmodclem2  12370  prodmodc  12371  qredeu  12901  pwbdvdseu  12973  nnmaxpwlemparts  12978  pcadd  13149  ballotfilemfc0  13291  ballotfilemfcc  13292  mhmpropd  13833  grprcan  13902  isnsg3  14070  ghmpreima  14129  rngpropd  14362  ringpropd  14451  islmodd  14739  lmodprop2d  14795  lss1d  14830  assamulgscmlem2  15152  mvrf1fi  15215  epttop  15328  txdis1cn  15516  metequiv2  15734  cncfmptc  15834  cncfmptid  15835  addccncf  15838  negcncf  15843  dedekindicclemicc  15870  mpodvdsmulf1o  16296  2sqlem5  16455  2sqlem9  16460