Theorem simplrl 541

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

Assertion

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

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 109	. 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  f1imass  5983  riota5f  6068  tfrexlem  6609  tfrcl  6639  nnsucuniel  6772  nntr2  6780  pw2f1odclem  7139  fopwdom  7141  fidceq  7176  fisbth  7192  fidcen  7208  fientri3  7227  unsnfidcex  7232  undifdc  7236  iunfidisj  7265  fiuni  7318  2omap  7325  ordiso2  7382  nninfninc  7470  acfun  7570  2omotaplemap  7630  ccfunen  7637  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  addcmpblnq0  7817  mulcmpblnq0  7818  prml  7851  addlocpr  7910  prmuloc  7940  mullocpr  7945  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemloc  7981  ltexprlemrl  7984  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  aptiprleml  8013  ltmprr  8016  cauappcvgprlemopl  8020  cauappcvgprlemopu  8022  cauappcvgprlemloc  8026  caucvgprlemopl  8043  caucvgprlemopu  8045  caucvgprlemloc  8049  caucvgprprlemopu  8073  caucvgprprlemloc  8077  caucvgprprlemexbt  8080  caucvgprprlemaddq  8082  suplocexprlemrl  8091  suplocexprlemdisj  8094  suplocexprlemloc  8095  suplocexprlemub  8097  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  ltsrprg  8121  mulgt0sr  8152  caucvgsrlemgt1  8169  suplocsrlemb  8180  axmulcl  8240  axcaucvglemres  8273  axpre-suploclemres  8275  axpre-suploc  8276  cnegexlem1  8509  negeu  8525  add20  8810  apreap  8924  cru  8939  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  mulge0  8956  mulap0  8991  divdivdivap  9052  prodgt0  9191  ltmul12a  9199  lt2mul2div  9218  ledivdiv  9229  lediv12a  9233  qapne  10056  xleadd1a  10293  ixxss12  10326  elfz0ubfz0  10550  qtri3or  10693  exbtwnzlemstep  10700  exbtwnzlemex  10702  exbtwnz  10703  rebtwn2zlemstep  10705  rebtwn2z  10707  btwnzge0  10757  iseqf1olemqf1o  10965  mulexpzap  11038  leexp1a  11053  hashen  11246  fihashdom  11266  hashun  11268  hashf1lem2  11309  swrdccatin1  11520  pfxccatin12lem3  11527  pfxccat3  11529  cjap  11695  cvg1nlemres  11774  rsqrmo  11816  abslt  11878  abs3lem  11901  cau3lem  11904  rexanre  12010  xrmaxltsup  12050  climcau  12139  sumeq2  12151  summodc  12176  fisumss  12185  fsum2d  12228  fsumabs  12258  fsumiun  12270  prodeq2  12350  prodmodclem2  12370  fprodcl2lem  12398  fprodap0  12414  fprod2d  12416  fprodrec  12422  fprodap0f  12429  fprodle  12433  eirrap  12571  divalglemeunn  12714  divalglemeuneg  12716  bezoutlemnewy  12799  bezoutlemstep  12800  bezoutlemmain  12801  bezoutlembi  12808  bezoutlemeu  12810  qredeu  12901  isprm5lem  12946  pwbdvdseu  12973  sqrt2irrap  12986  pythagtriplem2  13075  pythagtrip  13092  pclemub  13096  pcqmul  13112  pcexp  13118  pcneg  13134  pcprmpw2  13142  pcadd  13149  prmpwdvds  13164  4sqlem13m  13212  ballotfilemsf1o  13316  ennnfonelemg  13353  ennnfonelemrnh  13366  ctiunctlemfo  13389  nninfdclemf1  13402  imasival  13687  sgrppropd  13788  ismndd  13810  mndpropd  13813  mhmeql  13859  mhmmnd  13979  mulgfng  13987  issubg4m  14056  ssnmz  14074  conjnmzb  14143  gsumvalfi  14243  rngpropd  14362  ringpropd  14451  dvdsrtr  14518  aprlring  14710  islmod  14737  assapropd  15124  psrbaglefifi  15177  mplsubgfilemcl  15227  restbasg  15406  cnpnei  15457  cnptoprest2  15478  cnpdis  15480  lmtopcnp  15488  txcnp  15509  ismet2  15592  blininf  15662  metss2lem  15735  xmettxlem  15747  xmettx  15748  metcnp  15750  metcnpi3  15755  addcncntoplem  15799  fsumcncntop  15805  mulc1cncf  15827  cncfco  15829  mulcncf  15846  dedekindeulemuub  15855  dedekindeu  15861  dedekindicclemuub  15864  ivthinclemloc  15879  ivthinc  15881  limcimo  15903  limccnp2cntop  15915  dveflem  15964  plyf  15975  plyco  15997  plycj  15999  dvply2g  16004  logbgcd1irrap  16218  zprmlogbap  16230  perfectlem2  16312  lgsdilem  16363  lgsquad2lem2  16418  lgsquad3  16420  2sqlem5  16455  2sqlem9  16460  usgredg4  16673  usgr1eop  16703  usgr1vr  16706  subuhgr  16730  subumgr  16732  subusgr  16733  clwwlknonex2lem2  16896  pw1map  17242  qdencn  17290  apdiff  17316  qdiff  17317