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

Theorem 3adantl3 1148
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3adantl.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
3adantl3 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adantl3
StepHypRef Expression
1 3simpa 1128 . 2 ((𝜑𝜓𝜏) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 572 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  w3a 1068
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 199  df-an 388  df-3an 1070
This theorem is referenced by:  dif1en  8548  infpssrlem4  9528  fin23lem11  9539  tskwun  10006  gruf  10033  lediv2a  11337  prunioo  12686  nn0p1elfzo  12898  hashunsnggt  13571  rpnnen2lem7  15436  muldvds1  15497  muldvds2  15498  dvdscmul  15499  dvdsmulc  15500  rpexp  15923  pospropd  17605  mdetmul  20939  elcls  21388  iscnp4  21578  cnpnei  21579  cnpflf2  22315  cnpflf  22316  cnpfcf  22356  xbln0  22730  blcls  22822  iimulcl  23247  icccvx  23260  iscau2  23586  rrxcph  23701  cncombf  23965  mumul  25463  ax5seglem1  26420  ax5seglem2  26421  clwwlkinwwlk  27558  clwwlkinwwlkOLD  27559  nvmul0or  28207  fh1  29179  fh2  29180  cm2j  29181  pjoi0  29278  hoadddi  29364  hmopco  29584  padct  30210  iocinif  30259  volfiniune  31134  eulerpartlemb  31271  ivthALT  33204  lindsadd  34326  cnambfre  34381  rngohomco  34694  rngoisoco  34702  pexmidlem3N  36553  hdmapglem7  38510  relexpmulg  39418  supxrgere  41031  supxrgelem  41035  supxrge  41036  infxr  41065  infleinflem2  41069  rexabslelem  41124  lptre2pt  41353  fnlimfvre  41387  limsupmnfuzlem  41439  climisp  41459  limsupgtlem  41490  dvnprodlem1  41662  ibliccsinexp  41667  iblioosinexp  41669  fourierdlem12  41836  fourierdlem41  41865  fourierdlem42  41866  fourierdlem48  41871  fourierdlem49  41872  fourierdlem51  41874  fourierdlem73  41896  fourierdlem74  41897  fourierdlem75  41898  fourierdlem97  41920  etransclem24  41975  ioorrnopnlem  42021  issalnnd  42060  sge0rpcpnf  42135  sge0seq  42160  meaiuninc3v  42198  smfmullem4  42501  smflimsupmpt  42535  smfliminfmpt  42538  lincdifsn  43847
  Copyright terms: Public domain W3C validator