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  4497  fcofo  5993  acexmid  6087  rdgon  6661  oawordi  6746  nnmord  6794  nnmword  6795  1dom1el  7112  mapunen  7156  fidifsnen  7177  dif1en  7188  ac6sfi  7207  fissfi  7268  difinfsn  7447  2omotaplemap  7630  enq0tr  7808  distrlem4prl  7958  distrlem4pru  7959  ltaprg  7993  lelttr  8421  ltletr  8422  readdcan  8474  addcan  8514  addcan2  8515  ltadd2  8755  divmulassap  9034  indfdc  9308  xrlelttr  10226  xrltletr  10227  xaddass  10289  xleadd1a  10293  xlesubadd  10303  icoshftf1o  10411  lincmble  10424  difelfzle  10559  fzo1fzo0n0  10613  modqmuladdim  10826  modqmuladdnn0  10827  modqm1p1mod0  10834  q2submod  10844  modifeq2int  10845  modqaddmulmod  10850  seq1g  10922  seqp1g  10925  ltexp2a  11050  exple1  11054  expnlbnd2  11125  nn0ltexp2  11170  nn0leexp2  11171  mulsubdivbinom2ap  11172  expcan  11177  fiprsshashgt1  11281  hashtpgim  11320  hashtpg  11322  fun2dmnop0  11325  ccatass  11399  fzowrddc  11442  swrdclg  11445  ccatopth  11511  pfxccatin12lem2a  11522  pfxccat3  11529  maxleastb  12004  maxltsup  12008  xrltmaxsup  12049  xrmaxltsup  12050  xrmaxaddlem  12052  xrmaxadd  12053  addcn2  12102  mulcn2  12104  isumz  12182  dvdsmodexp  12588  modmulconst  12616  dvdsmod  12655  divalglemex  12715  divalg  12717  gcdass  12818  rplpwr  12830  rppwr  12831  nnwodc  12839  uzwodc  12840  rpmulgcd2  12899  rpdvds  12903  rpexp  12958  znege1  12984  prmdiveq  13044  hashgcdlem  13046  coprimeprodsq  13066  coprimeprodsq2  13067  pythagtriplem3  13076  pcdvdsb  13129  pcgcd1  13137  dvdsprmpweq  13144  pcbc  13160  ctinf  13380  nninfdc  13403  isnsgrp  13781  issubmnd  13815  mulgnn0p1  13996  mulgnnsubcl  13997  mulgneg  14003  mulgdirlem  14016  nmzsubg  14073  ghmmulg  14119  gsumsncmn  14247  ring1eq0  14461  rmodislmod  14798  lspss  14846  2idlcpblrng  14970  issubassa  15123  aspss  15129  snifpsrbagfi  15170  neiint  15383  topssnei  15400  cnptopco  15460  cnrest2  15474  cnptoprest  15477  upxp  15510  bldisj  15639  blgt0  15640  bl2in  15641  blss2ps  15644  blss2  15645  xblm  15655  blssps  15665  blss  15666  bdmopn  15742  metcnp2  15751  txmetcnp  15756  cncfmptc  15834  dvcnp2cntop  15937  dvcn  15938  ply1term  15981  dvply1  16003  logdivlti  16123  ltexp2  16189  pellexlem2  16242  bcmono  16316  lgsfvalg  16341  lgsneg  16360  lgsmod  16362  lgsdilem  16363  lgsdirprm  16370  lgsdir  16371  lgsdi  16373  lgsne0  16374