Theorem simpl3 1029

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

Assertion

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

Proof of Theorem simpl3

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

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

This theorem is referenced by:  simpll3  1065  simprl3  1071  simp1l3  1119  simp2l3  1125  simp3l3  1131  3anandirs  1385  ifnetruedc  3665  frirrg  4470  fcofo  5956  acexmid  6048  rdgon  6616  oawordi  6701  nnmord  6749  nnmword  6750  1dom1el  7059  mapunen  7103  fidifsnen  7124  dif1en  7135  ac6sfi  7154  fissfi  7215  difinfsn  7390  2omotaplemap  7567  enq0tr  7745  distrlem4prl  7895  distrlem4pru  7896  ltaprg  7930  lelttr  8358  ltletr  8359  readdcan  8409  addcan  8449  addcan2  8450  ltadd2  8689  divmulassap  8965  xrlelttr  10135  xrltletr  10136  xaddass  10198  xleadd1a  10202  xlesubadd  10212  icoshftf1o  10320  lincmble  10333  difelfzle  10464  fzo1fzo0n0  10518  modqmuladdim  10725  modqmuladdnn0  10726  modqm1p1mod0  10733  q2submod  10743  modifeq2int  10744  modqaddmulmod  10749  seq1g  10821  seqp1g  10824  ltexp2a  10949  exple1  10953  expnlbnd2  11023  nn0ltexp2  11067  nn0leexp2  11068  mulsubdivbinom2ap  11069  expcan  11074  fiprsshashgt1  11177  hashtpgim  11210  hashtpg  11212  fun2dmnop0  11215  ccatass  11289  fzowrddc  11332  swrdclg  11335  ccatopth  11401  pfxccatin12lem2a  11412  pfxccat3  11419  maxleastb  11892  maxltsup  11896  xrltmaxsup  11935  xrmaxltsup  11936  xrmaxaddlem  11938  xrmaxadd  11939  addcn2  11988  mulcn2  11990  isumz  12068  dvdsmodexp  12474  modmulconst  12502  dvdsmod  12541  divalglemex  12601  divalg  12603  gcdass  12704  rplpwr  12716  rppwr  12717  nnwodc  12725  uzwodc  12726  rpmulgcd2  12785  rpdvds  12789  rpexp  12843  znege1  12868  prmdiveq  12926  hashgcdlem  12928  coprimeprodsq  12948  coprimeprodsq2  12949  pythagtriplem3  12958  pcdvdsb  13011  pcgcd1  13019  dvdsprmpweq  13026  pcbc  13042  ctinf  13170  nninfdc  13193  isnsgrp  13608  issubmnd  13644  mulgnn0p1  13839  mulgnnsubcl  13840  mulgneg  13846  mulgdirlem  13859  nmzsubg  13916  ghmmulg  13962  ring1eq0  14181  rmodislmod  14486  lspss  14534  2idlcpblrng  14658  neiint  14997  topssnei  15014  cnptopco  15074  cnrest2  15088  cnptoprest  15091  upxp  15124  bldisj  15253  blgt0  15254  bl2in  15255  blss2ps  15258  blss2  15259  xblm  15269  blssps  15279  blss  15280  bdmopn  15356  metcnp2  15365  txmetcnp  15370  cncfmptc  15448  dvcnp2cntop  15551  dvcn  15552  ply1term  15595  dvply1  15617  logdivlti  15733  ltexp2  15793  pellexlem2  15833  lgsfvalg  15865  lgsneg  15884  lgsmod  15886  lgsdilem  15887  lgsdirprm  15894  lgsdir  15895  lgsdi  15897  lgsne0  15898  gfsumsn  16853