MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant1r Structured version   Visualization version   GIF version

Theorem 3adant1r 1359
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant1r (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)

Proof of Theorem 3adant1r
StepHypRef Expression
1 3adant1l.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213expb 1285 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
32adantlr 751 . 2 (((𝜑𝜏) ∧ (𝜓𝜒)) → 𝜃)
433impb 1279 1 (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1056
This theorem is referenced by:  3adant2r  1361  3adant3r  1363  ecopovtrn  7893  isf32lem9  9221  axdc3lem4  9313  tskun  9646  dvdscmulr  15057  divalglem8  15170  ghmgrp  17586  quscrng  19288  dvfsumlem3  23836  dvfsumrlim  23839  dvfsumrlim2  23840  dvfsumrlim3  23841  dchrisumlem3  25225  dchrisum  25226  abvcxp  25349  padicabv  25364  hvmulcan  28057  isarchi2  29867  archiabllem2c  29877  hasheuni  30275  carsgclctunlem1  30507  carsggect  30508  carsgclctunlem2  30509  carsgclctunlem3  30510  carsgclctun  30511  carsgsiga  30512  omsmeas  30513  tendoicl  36401  cdlemkfid2N  36528  erngdvlem4  36596  pellex  37716  refsumcn  39503  restuni3  39615  wessf1ornlem  39685  unirnmapsn  39720  ssmapsn  39722  iunmapsn  39723  ssfiunibd  39837  supxrgelem  39866  infleinf2  39954  fmuldfeq  40133  limsupmnfuzlem  40276  limsupre3uzlem  40285  cosknegpi  40398  icccncfext  40418  stoweidlem31  40566  stoweidlem43  40578  stoweidlem46  40581  stoweidlem52  40587  stoweidlem53  40588  stoweidlem54  40589  stoweidlem55  40590  stoweidlem56  40591  stoweidlem57  40592  stoweidlem58  40593  stoweidlem59  40594  stoweidlem60  40595  stoweidlem62  40597  stoweid  40598  fourierdlem12  40654  fourierdlem41  40683  fourierdlem48  40689  fourierdlem79  40720  fourierdlem81  40722  etransclem24  40793  etransclem46  40815  sge0f1o  40917  sge0iunmptlemre  40950  sge0iunmpt  40953  sge0seq  40981  caragenfiiuncl  41050  hoicvr  41083  hoidmvval0  41122  hspmbllem2  41162  smflimsuplem7  41353  el0ldep  42580
  Copyright terms: Public domain W3C validator