Theorem simpr1 1030

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

Assertion

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

Proof of Theorem simpr1

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

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

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 1007

This theorem is referenced by:  simplr1  1066  simprr1  1072  simp1r1  1120  simp2r1  1126  simp3r1  1132  3anandis  1384  isopolem  5994  caovlem2d  6246  suppfnss  6456  tfrlemibacc  6556  tfrlemibfn  6558  tfr1onlembacc  6572  tfr1onlembfn  6574  tfrcllembacc  6585  tfrcllembfn  6587  eqsupti  7286  prmuloc2  7878  ltntri  8397  elioc2  10265  elico2  10266  elicc2  10267  fseq1p1m1  10424  elfz0ubfz0  10455  ico0  10617  seq3f1olemp  10873  seq3f1oleml  10874  bcval5  11121  hashtpgim  11210  swrdsbslen  11351  ccatswrd  11355  isumss2  12072  tanaddap  12418  dvds2ln  12503  divalglemeunn  12600  divalglemex  12601  divalglemeuneg  12602  qredeq  12786  pcdvdstr  13018  isstructr  13216  prdssgrpd  13617  prdsmndd  13650  imasmnd2  13654  mndissubm  13677  grpsubrcan  13783  grpsubadd  13790  grpsubsub  13791  grpaddsubass  13792  grpsubsub4  13795  grpnnncan2  13799  imasgrp2  13816  mulgnndir  13857  mulgnn0dir  13858  mulgdir  13860  mulgnnass  13863  mulgnn0ass  13864  mulgass  13865  mulgsubdir  13868  issubg2m  13895  eqgval  13929  qusgrp  13938  kerf1ghm  13980  cmn32  14010  cmn12  14012  abladdsub  14021  rngass  14072  imasrng  14089  srgass  14104  ringdilem  14145  ringass  14149  imasring  14197  opprrng  14210  opprring  14212  mulgass3  14218  unitgrp  14250  dvrass  14273  dvrdir  14277  subrgunit  14373  issubrg2  14375  aprap  14421  islss3  14514  sralmod  14585  icnpimaex  15063  cnptopresti  15090  upxp  15124  psmettri  15182  isxmet2d  15200  xmettri  15224  metrtri  15229  xmetres2  15231  bldisj  15253  blss2ps  15258  blss2  15259  xmstri2  15322  mstri2  15323  xmstri  15324  mstri  15325  xmstri3  15326  mstri3  15327  msrtri  15328  comet  15351  bdbl  15355  xmetxp  15359  dvconst  15546  dvconstre  15548  dvconstss  15550  sgmmul  15851  findset  16702  pw1ndom3  16751