Theorem simpl3 1004

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

Assertion

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

Proof of Theorem simpl3

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

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

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 982

This theorem is referenced by:  simpll3  1040  simprl3  1046  simp1l3  1094  simp2l3  1100  simp3l3  1106  3anandirs  1359  ifnetruedc  3599  frirrg  4382  fcofo  5828  acexmid  5918  rdgon  6441  oawordi  6524  nnmord  6572  nnmword  6573  fidifsnen  6928  dif1en  6937  ac6sfi  6956  difinfsn  7161  2omotaplemap  7319  enq0tr  7496  distrlem4prl  7646  distrlem4pru  7647  ltaprg  7681  lelttr  8110  ltletr  8111  readdcan  8161  addcan  8201  addcan2  8202  ltadd2  8440  divmulassap  8716  xrlelttr  9875  xrltletr  9876  xaddass  9938  xleadd1a  9942  xlesubadd  9952  icoshftf1o  10060  difelfzle  10203  fzo1fzo0n0  10253  modqmuladdim  10441  modqmuladdnn0  10442  modqm1p1mod0  10449  q2submod  10459  modifeq2int  10460  modqaddmulmod  10465  seq1g  10537  seqp1g  10540  ltexp2a  10665  exple1  10669  expnlbnd2  10739  nn0ltexp2  10783  nn0leexp2  10784  mulsubdivbinom2ap  10785  expcan  10790  fiprsshashgt1  10891  maxleastb  11361  maxltsup  11365  xrltmaxsup  11403  xrmaxltsup  11404  xrmaxaddlem  11406  xrmaxadd  11407  addcn2  11456  mulcn2  11458  isumz  11535  dvdsmodexp  11941  modmulconst  11969  dvdsmod  12007  divalglemex  12066  divalg  12068  gcdass  12155  rplpwr  12167  rppwr  12168  nnwodc  12176  uzwodc  12177  rpmulgcd2  12236  rpdvds  12240  rpexp  12294  znege1  12319  prmdiveq  12377  hashgcdlem  12379  coprimeprodsq  12398  coprimeprodsq2  12399  pythagtriplem3  12408  pcdvdsb  12461  pcgcd1  12469  dvdsprmpweq  12476  pcbc  12492  ctinf  12590  nninfdc  12613  isnsgrp  12992  issubmnd  13026  mulgnn0p1  13206  mulgnnsubcl  13207  mulgneg  13213  mulgdirlem  13226  nmzsubg  13283  ghmmulg  13329  ring1eq0  13547  rmodislmod  13850  lspss  13898  2idlcpblrng  14022  neiint  14324  topssnei  14341  cnptopco  14401  cnrest2  14415  cnptoprest  14418  upxp  14451  bldisj  14580  blgt0  14581  bl2in  14582  blss2ps  14585  blss2  14586  xblm  14596  blssps  14606  blss  14607  bdmopn  14683  metcnp2  14692  txmetcnp  14697  cncfmptc  14775  dvcnp2cntop  14878  dvcn  14879  ply1term  14922  dvply1  14943  logdivlti  15057  ltexp2  15115  lgsfvalg  15162  lgsneg  15181  lgsmod  15183  lgsdilem  15184  lgsdirprm  15191  lgsdir  15192  lgsdi  15194  lgsne0  15195  1dom1el  15553