Theorem simpr3 1036

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

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

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simp3 1030	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
2	1	adantl 277	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1009

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

This theorem depends on definitions:  df-bi 117  df-3an 1011

This theorem is referenced by:  simplr3  1072  simprr3  1078  simp1r3  1126  simp2r3  1132  simp3r3  1138  3anandis  1388  isopolem  6022  suppfnss  6491  tfrlemibacc  6591  tfrlemibxssdm  6592  tfrlemibfn  6593  tfr1onlembacc  6607  tfr1onlembxssdm  6608  tfr1onlembfn  6609  tfrcllembacc  6620  tfrcllembxssdm  6621  tfrcllembfn  6622  elfir  7301  prloc  7852  prmuloc2  7928  ltntri  8448  eluzuzle  9913  xlesubadd  10268  elioc2  10321  elico2  10322  elicc2  10323  fseq1p1m1  10484  seq3f1olemp  10935  seq3f1oleml  10936  bcval5  11184  hashdifpr  11244  hashtpgim  11280  ccatswrd  11425  pfxccat3a  11493  isumss2  12143  tanaddap  12489  dvds2ln  12574  divalglemeunn  12671  divalglemex  12672  divalglemeuneg  12673  f1ovscpbl  13616  imasmnd2  13742  imasmnd  13743  grpsubadd  13876  grpaddsubass  13878  grpsubsub4  13881  grppnpcan2  13882  grpnpncan  13883  grpnnncan2  13885  imasgrp2  13896  imasgrp  13897  mulgnndir  13937  mulgnn0dir  13938  mulgnnass  13943  mulgnn0ass  13944  mulgass  13945  issubg2m  13975  qusgrp  14018  kerf1ghm  14060  cmn32  14090  cmn12  14092  abladdsub  14102  ablsubsub23  14112  prdssgrpd  14174  prdsmndd  14177  rngass  14221  imasrng  14238  srgdilem  14256  srgass  14258  ringdilem  14299  ringass  14303  ringrng  14324  imasring  14352  opprrng  14365  opprring  14367  mulgass3  14374  unitgrp  14406  dvrass  14429  dvrdir  14433  subrgunit  14530  issubrg2  14532  aprap  14581  lss1  14682  lsssn0  14690  islss3  14699  sralmod  14770  restopnb  15265  icnpimaex  15295  cnptopresti  15322  psmettri  15414  isxmet2d  15432  xmettri  15456  metrtri  15461  xmetres2  15463  bldisj  15485  blss2ps  15490  blss2  15491  xmstri2  15554  mstri2  15555  xmstri  15556  mstri  15557  xmstri3  15558  mstri3  15559  msrtri  15560  comet  15583  bdbl  15587  xmetxp  15591  dvconst  15778  dvconstre  15780  dvconstss  15782  sgmmul  16093  pw1ndom3  17003