Theorem simpl1 1024

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

Assertion

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

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 1021	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	adantr 276	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

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

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 1004

This theorem is referenced by:  simpll1  1060  simprl1  1066  simp1l1  1114  simp2l1  1120  simp3l1  1126  3anandirs  1382  rspc3ev  2924  brcogw  4894  cocan1  5920  oawordi  6628  nnmord  6676  nnmword  6677  dif1en  7054  ac6sfi  7073  ordiso2  7218  difinfsn  7283  ctssdc  7296  2omotaplemap  7459  enq0tr  7637  distrlem4prl  7787  distrlem4pru  7788  ltaprg  7822  aptiprlemu  7843  lelttr  8251  readdcan  8302  addcan  8342  addcan2  8343  ltadd2  8582  ltmul1a  8754  ltmul1  8755  divmulassap  8858  divmulasscomap  8859  lemul1a  9021  xrlelttr  10019  xleadd1a  10086  xlesubadd  10096  icoshftf1o  10204  lincmb01cmp  10216  iccf1o  10217  fztri3or  10252  fzofzim  10405  ioom  10497  modqmuladdim  10606  modqm1p1mod0  10614  q2submod  10624  modqaddmulmod  10630  ltexp2a  10830  exple1  10834  expnlbnd2  10904  nn0ltexp2  10948  nn0leexp2  10949  expcan  10955  fiprsshashgt1  11057  fimaxq  11067  fun2dmnop0  11087  ccatass  11161  swrdlen  11205  swrdfv  11206  swrdswrdlem  11257  ccatopth  11269  maxleastb  11746  maxltsup  11750  xrltmaxsup  11789  xrmaxltsup  11790  xrmaxaddlem  11792  addcn2  11842  mulcn2  11844  dvdsmodexp  12327  dvdsadd2b  12372  dvdsmod  12394  oexpneg  12409  divalglemex  12454  divalg  12456  gcdass  12557  rplpwr  12569  rppwr  12570  nnwodc  12578  coprmdvds2  12636  rpmulgcd2  12638  qredeq  12639  rpdvds  12642  cncongr2  12647  rpexp  12696  znege1  12721  prmdiveq  12779  hashgcdlem  12781  odzdvds  12789  modprmn0modprm0  12800  coprimeprodsq2  12802  pythagtriplem3  12811  pcdvdsb  12864  pcgcd1  12872  qexpz  12896  pockthg  12901  ctinf  13022  nninfdc  13045  unbendc  13046  isnsgrp  13460  issubmnd  13496  ress0g  13497  mulgneg  13698  mulgdirlem  13711  submmulg  13724  subgmulg  13746  nmzsubg  13768  ghmmulg  13814  srg1zr  13971  ring1eq0  14032  mulgass2  14042  rhmdvdsr  14160  rmodislmodlem  14335  rmodislmod  14336  lssintclm  14369  rnglidlrng  14483  2idlcpblrng  14508  neiint  14840  topssnei  14857  iscnp4  14913  cnptopco  14917  cnconst2  14928  cnrest2  14931  cnptoprest  14934  cnpdis  14937  bldisj  15096  blgt0  15097  bl2in  15098  blss2ps  15101  blss2  15102  xblm  15112  blssps  15122  blss  15123  xmetresbl  15135  bdbl  15198  metcnp3  15206  metcnp2  15208  cncfmptc  15291  dvcnp2cntop  15394  dvcn  15395  logdivlti  15576  ltexp2  15636  lgsfcl2  15706  lgsdilem  15727  lgsdirprm  15734  lgsdir  15735  lgsdi  15737  lgsne0  15738  incistruhgr  15911  clwwlkext2edg  16190