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 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

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

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 1011

This theorem is referenced by:  simpll3  1069  simprl3  1075  simp1l3  1123  simp2l3  1129  simp3l3  1135  3anandirs  1389  ifnetruedc  3684  frirrg  4493  fcofo  5984  acexmid  6078  rdgon  6651  oawordi  6736  nnmord  6784  nnmword  6785  1dom1el  7101  mapunen  7145  fidifsnen  7166  dif1en  7177  ac6sfi  7196  fissfi  7257  difinfsn  7434  2omotaplemap  7617  enq0tr  7795  distrlem4prl  7945  distrlem4pru  7946  ltaprg  7980  lelttr  8408  ltletr  8409  readdcan  8460  addcan  8500  addcan2  8501  ltadd2  8741  divmulassap  9019  xrlelttr  10191  xrltletr  10192  xaddass  10254  xleadd1a  10258  xlesubadd  10268  icoshftf1o  10376  lincmble  10389  difelfzle  10524  fzo1fzo0n0  10578  modqmuladdim  10787  modqmuladdnn0  10788  modqm1p1mod0  10795  q2submod  10805  modifeq2int  10806  modqaddmulmod  10811  seq1g  10883  seqp1g  10886  ltexp2a  11011  exple1  11015  expnlbnd2  11086  nn0ltexp2  11130  nn0leexp2  11131  mulsubdivbinom2ap  11132  expcan  11137  fiprsshashgt1  11241  hashtpgim  11280  hashtpg  11282  fun2dmnop0  11285  ccatass  11359  fzowrddc  11402  swrdclg  11405  ccatopth  11471  pfxccatin12lem2a  11482  pfxccat3  11489  maxleastb  11963  maxltsup  11967  xrltmaxsup  12006  xrmaxltsup  12007  xrmaxaddlem  12009  xrmaxadd  12010  addcn2  12059  mulcn2  12061  isumz  12139  dvdsmodexp  12545  modmulconst  12573  dvdsmod  12612  divalglemex  12672  divalg  12674  gcdass  12775  rplpwr  12787  rppwr  12788  nnwodc  12796  uzwodc  12797  rpmulgcd2  12856  rpdvds  12860  rpexp  12914  znege1  12939  prmdiveq  12997  hashgcdlem  12999  coprimeprodsq  13019  coprimeprodsq2  13020  pythagtriplem3  13029  pcdvdsb  13082  pcgcd1  13090  dvdsprmpweq  13097  pcbc  13113  ctinf  13304  nninfdc  13327  isnsgrp  13704  issubmnd  13738  mulgnn0p1  13919  mulgnnsubcl  13920  mulgneg  13926  mulgdirlem  13939  nmzsubg  13996  ghmmulg  14042  gsumsncmn  14139  ring1eq0  14336  rmodislmod  14671  lspss  14719  2idlcpblrng  14843  issubassa  14996  aspss  15002  neiint  15229  topssnei  15246  cnptopco  15306  cnrest2  15320  cnptoprest  15323  upxp  15356  bldisj  15485  blgt0  15486  bl2in  15487  blss2ps  15490  blss2  15491  xblm  15501  blssps  15511  blss  15512  bdmopn  15588  metcnp2  15597  txmetcnp  15602  cncfmptc  15680  dvcnp2cntop  15783  dvcn  15784  ply1term  15827  dvply1  15849  logdivlti  15965  ltexp2  16026  pellexlem2  16075  lgsfvalg  16107  lgsneg  16126  lgsmod  16128  lgsdilem  16129  lgsdirprm  16136  lgsdir  16137  lgsdi  16139  lgsne0  16140