Theorem simplrr 542

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

Assertion

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

Proof of Theorem simplrr

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 493	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:  rmob  3145  disjiun  4125  isotr  6022  riota5f  6065  tfrexlem  6605  tfrcl  6635  nnsucuniel  6768  pw2f1odclem  7134  fopwdom  7136  dif1enen  7184  fisbth  7187  fin0  7189  fin0or  7190  diffisn  7197  fidcen  7203  finexdc  7207  elssdc  7209  fientri3  7222  unfidisj  7229  undifdc  7231  ssfirab  7244  fnfi  7250  iunfidisj  7260  mapfi  7261  fissfi  7263  dcfi  7315  2omap  7319  ordiso2  7376  difinfinf  7442  ctmlemr  7449  exmidfodomrlemr  7555  2omotaplemap  7624  cc2lem  7633  cc3  7635  addcmpblnq  7735  mulcmpblnq  7736  ordpipqqs  7742  ltexnqq  7776  addcmpblnq0  7811  mulcmpblnq0  7812  prmu  7846  addlocpr  7904  prmuloc  7934  prmuloc2  7935  ltaddpr  7965  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemloc  7975  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  aptiprleml  8007  aptiprlemu  8008  ltmprr  8010  cauappcvgprlemloc  8020  archrecpr  8032  caucvgprlemloc  8043  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  suplocexprlemdisj  8088  suplocexprlemloc  8089  addcmpblnr  8107  mulcmpblnrlemg  8108  mulcmpblnr  8109  ltsrprg  8115  mulgt0sr  8146  caucvgsrlemgt1  8163  suplocsrlemb  8174  axmulcl  8234  axarch  8259  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  readdcan  8468  cnegexlem1  8503  negeu  8519  add20  8804  apreap  8918  cru  8933  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  divdivdivap  9046  ltmul12a  9193  lemul12a  9195  lt2mul2div  9212  ledivdiv  9223  lediv12a  9227  qapne  10049  xleadd1a  10286  ixxss12  10319  ioodisj  10406  fz0fzelfz0  10545  zsupcllemstep  10673  zsupssdc  10684  qtri3or  10686  exbtwnzlemstep  10693  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnre  10702  btwnzge0  10750  iseqf1olemqf1o  10958  mulexpzap  11031  leexp1a  11046  expnbnd  11116  hashen  11239  fihashdom  11259  hashun  11261  hashf1  11303  zfz1iso  11309  swrdccat  11523  reuccatpfxs1  11535  cjap  11688  cvg1nlemres  11767  rsqrmo  11809  abs3lem  11894  cau3lem  11897  rexanre  12003  fiidxsupcl  12012  xrmaxltsup  12043  climcau  12132  sumeq2  12144  summodc  12169  fsum3cvg3  12182  fsum2d  12221  prodeq2  12343  prodmodclem2  12363  fprod2d  12409  eirrap  12564  addmodlteqALT  12645  divalglemeunn  12707  divalglemeuneg  12709  bezoutlemnewy  12792  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlembi  12801  bezoutlemeu  12803  rpdvds  12896  isprm5lem  12939  isprm6  12945  pwbdvdslemn  12963  pwbdvdseu  12966  sqrt2irrap  12979  pythagtriplem2  13068  pythagtrip  13085  pclemub  13089  pcqmul  13105  pcexp  13111  pcneg  13127  pcprmpw2  13135  pcadd  13142  pcmpt  13145  4sqlem13m  13205  ballotfilemcdc  13275  ballotfilemfc0  13284  ballotfilemfcc  13285  ennnfonelemrnh  13359  ennnfonelemnn0  13365  ctinfomlemom  13370  ctiunctlemfo  13382  nninfdclemf1  13395  imasival  13680  sgrppropd  13781  ismndd  13803  mndpropd  13806  mhmeql  13852  mhmmnd  13972  issubg4m  14049  ssnmz  14067  conjnmzb  14136  gsumvalfi  14236  rngpropd  14338  ringpropd  14427  aprlring  14684  islmod  14711  assapropd  15098  psrval  15134  psrbaglefifi  15147  restbasg  15360  cnrest2  15428  cnpdis  15434  lmtopcnp  15442  txcnp  15463  txlm  15471  ismet2  15546  blininf  15616  metss2lem  15689  xmettxlem  15701  xmettx  15702  metcnp3  15703  metcnpi3  15709  addcncntoplem  15753  fsumcncntop  15759  mulcncf  15800  dedekindeulemuub  15809  dedekindeu  15815  dedekindicclemuub  15818  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthinclemloc  15833  ivthinc  15835  ivthdichlem  15843  limcimo  15857  limccnp2cntop  15869  plyf  15929  plyco  15951  plycj  15953  plyrecj  15955  dvply2g  15958  logdivlt  16090  logbgcd1irrap  16172  zprmlogbap  16184  perfectlem2  16266  lgsdilem  16317  lgsquad2lem2  16372  lgsquad3  16374  2sqlem5  16409  2sqlem9  16414  usgredg4  16627  usgr1vr  16660  subuhgr  16684  subumgr  16686  clwwlknonex2lem2  16850  eupth2lemsfi  16890  depindlem3  16920  qdencn  17243  apdiff  17269  qdiff  17270