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

Theorem 3adantl3 1211
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 1050 . 2 ((𝜑𝜓𝜏) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 486 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  dif1en  8055  infpssrlem4  8988  fin23lem11  8999  tskwun  9462  gruf  9489  lediv2a  10766  prunioo  12128  nn0p1elfzo  12333  rpnnen2lem7  14734  muldvds1  14790  muldvds2  14791  dvdscmul  14792  dvdsmulc  14793  rpexp  15216  pospropd  16903  mdetmul  20190  elcls  20629  iscnp4  20819  cnpnei  20820  cnpflf2  21556  cnpflf  21557  cnpfcf  21597  xbln0  21970  blcls  22062  iimulcl  22475  icccvx  22488  iscau2  22801  rrxcph  22905  cncombf  23148  mumul  24624  ax5seglem1  25526  ax5seglem2  25527  wwlkext2clwwlk  26097  nvmul0or  26677  fh1  27667  fh2  27668  cm2j  27669  pjoi0  27766  hoadddi  27852  hmopco  28072  padct  28691  iocinif  28739  volfiniune  29426  eulerpartlemb  29563  ivthALT  31306  cnambfre  32424  rngohomco  32739  rngoisoco  32747  pexmidlem3N  34072  hdmapglem7  36035  relexpmulg  36817  supxrgere  38287  supxrgelem  38291  supxrge  38292  infxr  38321  infleinflem2  38325  lptre2pt  38504  fnlimfvre  38538  dvnprodlem1  38633  ibliccsinexp  38639  iblioosinexp  38641  fourierdlem12  38809  fourierdlem41  38838  fourierdlem42  38839  fourierdlem48  38844  fourierdlem49  38845  fourierdlem51  38847  fourierdlem73  38869  fourierdlem74  38870  fourierdlem75  38871  fourierdlem97  38893  etransclem24  38948  ioorrnopnlem  38997  issalnnd  39036  sge0rpcpnf  39111  sge0seq  39136  smfmullem4  39476  wwlksext2clwwlk  41226  lincdifsn  42002
  Copyright terms: Public domain W3C validator