Theorem simpl1 1027

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

Assertion

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

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 1024	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	adantr 276	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

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

This theorem is referenced by:  simpll1  1063  simprl1  1069  simp1l1  1117  simp2l1  1123  simp3l1  1129  3anandirs  1385  rspc3ev  2941  brcogw  4929  cocan1  5966  oawordi  6715  nnmord  6763  nnmword  6764  mapunen  7117  dif1en  7149  ac6sfi  7168  ordiso2  7339  difinfsn  7404  ctssdc  7417  2omotaplemap  7587  enq0tr  7765  distrlem4prl  7915  distrlem4pru  7916  ltaprg  7950  aptiprlemu  7971  lelttr  8378  readdcan  8430  addcan  8470  addcan2  8471  ltadd2  8711  ltmul1a  8883  ltmul1  8884  divmulassap  8989  divmulasscomap  8990  lemul1a  9152  xrlelttr  10161  xleadd1a  10228  xlesubadd  10238  icoshftf1o  10346  lincmb01cmp  10358  lincmble  10359  iccf1o  10360  fztri3or  10396  nn0p1elfzo  10546  fzofzim  10552  ioom  10647  modqmuladdim  10756  modqm1p1mod0  10764  q2submod  10774  modqaddmulmod  10780  ltexp2a  10980  exple1  10984  expnlbnd2  11055  nn0ltexp2  11099  nn0leexp2  11100  expcan  11106  fiprsshashgt1  11210  fimaxq  11222  hashtpgim  11245  hashtpg  11247  fun2dmnop0  11250  ccatass  11324  swrdlen  11372  swrdfv  11373  swrdswrdlem  11424  ccatopth  11436  maxleastb  11927  maxltsup  11931  xrltmaxsup  11970  xrmaxltsup  11971  xrmaxaddlem  11973  addcn2  12023  mulcn2  12025  dvdsmodexp  12509  dvdsadd2b  12554  dvdsmod  12576  oexpneg  12591  divalglemex  12636  divalg  12638  gcdass  12739  rplpwr  12751  rppwr  12752  nnwodc  12760  coprmdvds2  12818  rpmulgcd2  12820  qredeq  12821  rpdvds  12824  cncongr2  12829  rpexp  12878  znege1  12903  prmdiveq  12961  hashgcdlem  12963  odzdvds  12971  modprmn0modprm0  12982  coprimeprodsq2  12984  pythagtriplem3  12993  pcdvdsb  13046  pcgcd1  13054  qexpz  13078  pockthg  13083  ctinf  13268  nninfdc  13291  unbendc  13292  isnsgrp  13672  issubmnd  13706  ress0g  13707  mulgneg  13896  mulgdirlem  13909  submmulg  13922  subgmulg  13944  nmzsubg  13966  ghmmulg  14012  ring1eq0  14294  mulgass2  14304  rhmdvdsr  14423  rmodislmodlem  14627  rmodislmod  14628  lssintclm  14661  rnglidlrng  14775  2idlcpblrng  14800  neiint  15139  topssnei  15156  iscnp4  15212  cnptopco  15216  cnconst2  15227  cnrest2  15230  cnptoprest  15233  cnpdis  15236  bldisj  15395  blgt0  15396  bl2in  15397  blss2ps  15400  blss2  15401  xblm  15411  blssps  15421  blss  15422  xmetresbl  15434  bdbl  15497  metcnp3  15505  metcnp2  15507  cncfmptc  15590  dvcnp2cntop  15693  dvcn  15694  logdivlti  15875  ltexp2  15935  pellexlem2  15975  lgsfcl2  16008  lgsdilem  16029  lgsdirprm  16036  lgsdir  16037  lgsdi  16039  lgsne0  16040  incistruhgr  16214  clwwlkext2edg  16546  clwwlknonex2e  16564