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  3668  frirrg  4473  fcofo  5959  acexmid  6051  rdgon  6619  oawordi  6704  nnmord  6752  nnmword  6753  1dom1el  7062  mapunen  7106  fidifsnen  7127  dif1en  7138  ac6sfi  7157  fissfi  7218  difinfsn  7393  2omotaplemap  7576  enq0tr  7754  distrlem4prl  7904  distrlem4pru  7905  ltaprg  7939  lelttr  8367  ltletr  8368  readdcan  8418  addcan  8458  addcan2  8459  ltadd2  8698  divmulassap  8974  xrlelttr  10145  xrltletr  10146  xaddass  10208  xleadd1a  10212  xlesubadd  10222  icoshftf1o  10330  lincmble  10343  difelfzle  10475  fzo1fzo0n0  10529  modqmuladdim  10736  modqmuladdnn0  10737  modqm1p1mod0  10744  q2submod  10754  modifeq2int  10755  modqaddmulmod  10760  seq1g  10832  seqp1g  10835  ltexp2a  10960  exple1  10964  expnlbnd2  11035  nn0ltexp2  11079  nn0leexp2  11080  mulsubdivbinom2ap  11081  expcan  11086  fiprsshashgt1  11190  hashtpgim  11225  hashtpg  11227  fun2dmnop0  11230  ccatass  11304  fzowrddc  11347  swrdclg  11350  ccatopth  11416  pfxccatin12lem2a  11427  pfxccat3  11434  maxleastb  11907  maxltsup  11911  xrltmaxsup  11950  xrmaxltsup  11951  xrmaxaddlem  11953  xrmaxadd  11954  addcn2  12003  mulcn2  12005  isumz  12083  dvdsmodexp  12489  modmulconst  12517  dvdsmod  12556  divalglemex  12616  divalg  12618  gcdass  12719  rplpwr  12731  rppwr  12732  nnwodc  12740  uzwodc  12741  rpmulgcd2  12800  rpdvds  12804  rpexp  12858  znege1  12883  prmdiveq  12941  hashgcdlem  12943  coprimeprodsq  12963  coprimeprodsq2  12964  pythagtriplem3  12973  pcdvdsb  13026  pcgcd1  13034  dvdsprmpweq  13041  pcbc  13057  ctinf  13202  nninfdc  13225  isnsgrp  13640  issubmnd  13676  mulgnn0p1  13871  mulgnnsubcl  13872  mulgneg  13878  mulgdirlem  13891  nmzsubg  13948  ghmmulg  13994  ring1eq0  14213  rmodislmod  14548  lspss  14596  2idlcpblrng  14720  neiint  15059  topssnei  15076  cnptopco  15136  cnrest2  15150  cnptoprest  15153  upxp  15186  bldisj  15315  blgt0  15316  bl2in  15317  blss2ps  15320  blss2  15321  xblm  15331  blssps  15341  blss  15342  bdmopn  15418  metcnp2  15427  txmetcnp  15432  cncfmptc  15510  dvcnp2cntop  15613  dvcn  15614  ply1term  15657  dvply1  15679  logdivlti  15795  ltexp2  15855  pellexlem2  15895  lgsfvalg  15927  lgsneg  15946  lgsmod  15948  lgsdilem  15949  lgsdirprm  15956  lgsdir  15957  lgsdi  15959  lgsne0  15960  gfsumsn  16916