Theorem simpl3 1026

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

Assertion

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

Proof of Theorem simpl3

Step	Hyp	Ref	Expression
1		simp3 1023	. 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  ax-ia3 108

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

This theorem is referenced by:  simpll3  1062  simprl3  1068  simp1l3  1116  simp2l3  1122  simp3l3  1128  3anandirs  1382  ifnetruedc  3647  frirrg  4445  fcofo  5920  acexmid  6012  rdgon  6547  oawordi  6632  nnmord  6680  nnmword  6681  1dom1el  6988  fidifsnen  7052  dif1en  7063  ac6sfi  7082  difinfsn  7293  2omotaplemap  7469  enq0tr  7647  distrlem4prl  7797  distrlem4pru  7798  ltaprg  7832  lelttr  8261  ltletr  8262  readdcan  8312  addcan  8352  addcan2  8353  ltadd2  8592  divmulassap  8868  xrlelttr  10034  xrltletr  10035  xaddass  10097  xleadd1a  10101  xlesubadd  10111  icoshftf1o  10219  difelfzle  10362  fzo1fzo0n0  10415  modqmuladdim  10622  modqmuladdnn0  10623  modqm1p1mod0  10630  q2submod  10640  modifeq2int  10641  modqaddmulmod  10646  seq1g  10718  seqp1g  10721  ltexp2a  10846  exple1  10850  expnlbnd2  10920  nn0ltexp2  10964  nn0leexp2  10965  mulsubdivbinom2ap  10966  expcan  10971  fiprsshashgt1  11074  fun2dmnop0  11104  ccatass  11178  fzowrddc  11221  swrdclg  11224  ccatopth  11290  pfxccatin12lem2a  11301  pfxccat3  11308  maxleastb  11768  maxltsup  11772  xrltmaxsup  11811  xrmaxltsup  11812  xrmaxaddlem  11814  xrmaxadd  11815  addcn2  11864  mulcn2  11866  isumz  11943  dvdsmodexp  12349  modmulconst  12377  dvdsmod  12416  divalglemex  12476  divalg  12478  gcdass  12579  rplpwr  12591  rppwr  12592  nnwodc  12600  uzwodc  12601  rpmulgcd2  12660  rpdvds  12664  rpexp  12718  znege1  12743  prmdiveq  12801  hashgcdlem  12803  coprimeprodsq  12823  coprimeprodsq2  12824  pythagtriplem3  12833  pcdvdsb  12886  pcgcd1  12894  dvdsprmpweq  12901  pcbc  12917  ctinf  13044  nninfdc  13067  isnsgrp  13482  issubmnd  13518  mulgnn0p1  13713  mulgnnsubcl  13714  mulgneg  13720  mulgdirlem  13733  nmzsubg  13790  ghmmulg  13836  ring1eq0  14054  rmodislmod  14358  lspss  14406  2idlcpblrng  14530  neiint  14862  topssnei  14879  cnptopco  14939  cnrest2  14953  cnptoprest  14956  upxp  14989  bldisj  15118  blgt0  15119  bl2in  15120  blss2ps  15123  blss2  15124  xblm  15134  blssps  15144  blss  15145  bdmopn  15221  metcnp2  15230  txmetcnp  15235  cncfmptc  15313  dvcnp2cntop  15416  dvcn  15417  ply1term  15460  dvply1  15482  logdivlti  15598  ltexp2  15658  lgsfvalg  15727  lgsneg  15746  lgsmod  15748  lgsdilem  15749  lgsdirprm  15756  lgsdir  15757  lgsdi  15759  lgsne0  15760