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  3603  frirrg  4386  fcofo  5834  acexmid  5924  rdgon  6453  oawordi  6536  nnmord  6584  nnmword  6585  fidifsnen  6940  dif1en  6949  ac6sfi  6968  difinfsn  7175  2omotaplemap  7340  enq0tr  7518  distrlem4prl  7668  distrlem4pru  7669  ltaprg  7703  lelttr  8132  ltletr  8133  readdcan  8183  addcan  8223  addcan2  8224  ltadd2  8463  divmulassap  8739  xrlelttr  9898  xrltletr  9899  xaddass  9961  xleadd1a  9965  xlesubadd  9975  icoshftf1o  10083  difelfzle  10226  fzo1fzo0n0  10276  modqmuladdim  10476  modqmuladdnn0  10477  modqm1p1mod0  10484  q2submod  10494  modifeq2int  10495  modqaddmulmod  10500  seq1g  10572  seqp1g  10575  ltexp2a  10700  exple1  10704  expnlbnd2  10774  nn0ltexp2  10818  nn0leexp2  10819  mulsubdivbinom2ap  10820  expcan  10825  fiprsshashgt1  10926  maxleastb  11396  maxltsup  11400  xrltmaxsup  11439  xrmaxltsup  11440  xrmaxaddlem  11442  xrmaxadd  11443  addcn2  11492  mulcn2  11494  isumz  11571  dvdsmodexp  11977  modmulconst  12005  dvdsmod  12044  divalglemex  12104  divalg  12106  gcdass  12207  rplpwr  12219  rppwr  12220  nnwodc  12228  uzwodc  12229  rpmulgcd2  12288  rpdvds  12292  rpexp  12346  znege1  12371  prmdiveq  12429  hashgcdlem  12431  coprimeprodsq  12451  coprimeprodsq2  12452  pythagtriplem3  12461  pcdvdsb  12514  pcgcd1  12522  dvdsprmpweq  12529  pcbc  12545  ctinf  12672  nninfdc  12695  isnsgrp  13108  issubmnd  13144  mulgnn0p1  13339  mulgnnsubcl  13340  mulgneg  13346  mulgdirlem  13359  nmzsubg  13416  ghmmulg  13462  ring1eq0  13680  rmodislmod  13983  lspss  14031  2idlcpblrng  14155  neiint  14465  topssnei  14482  cnptopco  14542  cnrest2  14556  cnptoprest  14559  upxp  14592  bldisj  14721  blgt0  14722  bl2in  14723  blss2ps  14726  blss2  14727  xblm  14737  blssps  14747  blss  14748  bdmopn  14824  metcnp2  14833  txmetcnp  14838  cncfmptc  14916  dvcnp2cntop  15019  dvcn  15020  ply1term  15063  dvply1  15085  logdivlti  15201  ltexp2  15261  lgsfvalg  15330  lgsneg  15349  lgsmod  15351  lgsdilem  15352  lgsdirprm  15359  lgsdir  15360  lgsdi  15362  lgsne0  15363  1dom1el  15721