Theorem simpl3 1033

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

Assertion

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

Proof of Theorem simpl3

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpll3  1069  simprl3  1075  simp1l3  1123  simp2l3  1129  simp3l3  1135  3anandirs  1389  ifnetruedc  3684  frirrg  4495  fcofo  5990  acexmid  6084  rdgon  6657  oawordi  6742  nnmord  6790  nnmword  6791  1dom1el  7107  mapunen  7151  fidifsnen  7172  dif1en  7183  ac6sfi  7202  fissfi  7263  difinfsn  7440  2omotaplemap  7623  enq0tr  7801  distrlem4prl  7951  distrlem4pru  7952  ltaprg  7986  lelttr  8414  ltletr  8415  readdcan  8466  addcan  8506  addcan2  8507  ltadd2  8747  divmulassap  9026  indfdc  9299  xrlelttr  10210  xrltletr  10211  xaddass  10273  xleadd1a  10277  xlesubadd  10287  icoshftf1o  10395  lincmble  10408  difelfzle  10543  fzo1fzo0n0  10597  modqmuladdim  10806  modqmuladdnn0  10807  modqm1p1mod0  10814  q2submod  10824  modifeq2int  10825  modqaddmulmod  10830  seq1g  10902  seqp1g  10905  ltexp2a  11030  exple1  11034  expnlbnd2  11105  nn0ltexp2  11149  nn0leexp2  11150  mulsubdivbinom2ap  11151  expcan  11156  fiprsshashgt1  11260  hashtpgim  11299  hashtpg  11301  fun2dmnop0  11304  ccatass  11378  fzowrddc  11421  swrdclg  11424  ccatopth  11490  pfxccatin12lem2a  11501  pfxccat3  11508  maxleastb  11982  maxltsup  11986  xrltmaxsup  12025  xrmaxltsup  12026  xrmaxaddlem  12028  xrmaxadd  12029  addcn2  12078  mulcn2  12080  isumz  12158  dvdsmodexp  12564  modmulconst  12592  dvdsmod  12631  divalglemex  12691  divalg  12693  gcdass  12794  rplpwr  12806  rppwr  12807  nnwodc  12815  uzwodc  12816  rpmulgcd2  12875  rpdvds  12879  rpexp  12933  znege1  12958  prmdiveq  13016  hashgcdlem  13018  coprimeprodsq  13038  coprimeprodsq2  13039  pythagtriplem3  13048  pcdvdsb  13101  pcgcd1  13109  dvdsprmpweq  13116  pcbc  13132  ctinf  13323  nninfdc  13346  isnsgrp  13723  issubmnd  13757  mulgnn0p1  13938  mulgnnsubcl  13939  mulgneg  13945  mulgdirlem  13958  nmzsubg  14015  ghmmulg  14061  gsumsncmn  14158  ring1eq0  14355  rmodislmod  14690  lspss  14738  2idlcpblrng  14862  issubassa  15015  aspss  15021  neiint  15248  topssnei  15265  cnptopco  15325  cnrest2  15339  cnptoprest  15342  upxp  15375  bldisj  15504  blgt0  15505  bl2in  15506  blss2ps  15509  blss2  15510  xblm  15520  blssps  15530  blss  15531  bdmopn  15607  metcnp2  15616  txmetcnp  15621  cncfmptc  15699  dvcnp2cntop  15802  dvcn  15803  ply1term  15846  dvply1  15868  logdivlti  15986  ltexp2  16049  pellexlem2  16098  bcmono  16124  lgsfvalg  16136  lgsneg  16155  lgsmod  16157  lgsdilem  16158  lgsdirprm  16165  lgsdir  16166  lgsdi  16168  lgsne0  16169