Theorem simpl3 1007

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

Assertion

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

Proof of Theorem simpl3

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

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

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 985

This theorem is referenced by:  simpll3  1043  simprl3  1049  simp1l3  1097  simp2l3  1103  simp3l3  1109  3anandirs  1363  ifnetruedc  3626  frirrg  4418  fcofo  5881  acexmid  5973  rdgon  6502  oawordi  6585  nnmord  6633  nnmword  6634  fidifsnen  7000  dif1en  7009  ac6sfi  7028  difinfsn  7235  2omotaplemap  7411  enq0tr  7589  distrlem4prl  7739  distrlem4pru  7740  ltaprg  7774  lelttr  8203  ltletr  8204  readdcan  8254  addcan  8294  addcan2  8295  ltadd2  8534  divmulassap  8810  xrlelttr  9970  xrltletr  9971  xaddass  10033  xleadd1a  10037  xlesubadd  10047  icoshftf1o  10155  difelfzle  10298  fzo1fzo0n0  10351  modqmuladdim  10556  modqmuladdnn0  10557  modqm1p1mod0  10564  q2submod  10574  modifeq2int  10575  modqaddmulmod  10580  seq1g  10652  seqp1g  10655  ltexp2a  10780  exple1  10784  expnlbnd2  10854  nn0ltexp2  10898  nn0leexp2  10899  mulsubdivbinom2ap  10900  expcan  10905  fiprsshashgt1  11006  fun2dmnop0  11036  ccatass  11109  fzowrddc  11145  swrdclg  11148  ccatopth  11214  pfxccatin12lem2a  11225  pfxccat3  11232  maxleastb  11691  maxltsup  11695  xrltmaxsup  11734  xrmaxltsup  11735  xrmaxaddlem  11737  xrmaxadd  11738  addcn2  11787  mulcn2  11789  isumz  11866  dvdsmodexp  12272  modmulconst  12300  dvdsmod  12339  divalglemex  12399  divalg  12401  gcdass  12502  rplpwr  12514  rppwr  12515  nnwodc  12523  uzwodc  12524  rpmulgcd2  12583  rpdvds  12587  rpexp  12641  znege1  12666  prmdiveq  12724  hashgcdlem  12726  coprimeprodsq  12746  coprimeprodsq2  12747  pythagtriplem3  12756  pcdvdsb  12809  pcgcd1  12817  dvdsprmpweq  12824  pcbc  12840  ctinf  12967  nninfdc  12990  isnsgrp  13405  issubmnd  13441  mulgnn0p1  13636  mulgnnsubcl  13637  mulgneg  13643  mulgdirlem  13656  nmzsubg  13713  ghmmulg  13759  ring1eq0  13977  rmodislmod  14280  lspss  14328  2idlcpblrng  14452  neiint  14784  topssnei  14801  cnptopco  14861  cnrest2  14875  cnptoprest  14878  upxp  14911  bldisj  15040  blgt0  15041  bl2in  15042  blss2ps  15045  blss2  15046  xblm  15056  blssps  15066  blss  15067  bdmopn  15143  metcnp2  15152  txmetcnp  15157  cncfmptc  15235  dvcnp2cntop  15338  dvcn  15339  ply1term  15382  dvply1  15404  logdivlti  15520  ltexp2  15580  lgsfvalg  15649  lgsneg  15668  lgsmod  15670  lgsdilem  15671  lgsdirprm  15678  lgsdir  15679  lgsdi  15681  lgsne0  15682  1dom1el  16264