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

Theorem 3adantl3 1202
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 1171 . 2 ((𝜑𝜓𝜏) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 571 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  dif1en  8426  infpssrlem4  9407  fin23lem11  9418  tskwun  9885  gruf  9912  lediv2a  11196  prunioo  12518  nn0p1elfzo  12729  rpnnen2lem7  15163  muldvds1  15223  muldvds2  15224  dvdscmul  15225  dvdsmulc  15226  rpexp  15643  pospropd  17333  mdetmul  20634  elcls  21085  iscnp4  21275  cnpnei  21276  cnpflf2  22011  cnpflf  22012  cnpfcf  22052  xbln0  22426  blcls  22518  iimulcl  22943  icccvx  22956  iscau2  23281  rrxcph  23386  cncombf  23633  mumul  25115  ax5seglem1  26016  ax5seglem2  26017  clwwlkinwwlk  27183  wwlksext2clwwlkOLD  27202  nvmul0or  27827  fh1  28799  fh2  28800  cm2j  28801  pjoi0  28898  hoadddi  28984  hmopco  29204  padct  29818  iocinif  29864  volfiniune  30612  eulerpartlemb  30749  ivthALT  32645  cnambfre  33764  rngohomco  34078  rngoisoco  34086  pexmidlem3N  35746  hdmapglem7  37704  relexpmulg  38496  supxrgere  40023  supxrgelem  40027  supxrge  40028  infxr  40057  infleinflem2  40061  rexabslelem  40118  lptre2pt  40346  fnlimfvre  40380  limsupmnfuzlem  40432  climisp  40452  limsupgtlem  40483  dvnprodlem1  40635  ibliccsinexp  40640  iblioosinexp  40642  fourierdlem12  40809  fourierdlem41  40838  fourierdlem42  40839  fourierdlem48  40844  fourierdlem49  40845  fourierdlem51  40847  fourierdlem73  40869  fourierdlem74  40870  fourierdlem75  40871  fourierdlem97  40893  etransclem24  40948  ioorrnopnlem  40997  issalnnd  41036  sge0rpcpnf  41111  sge0seq  41136  meaiuninc3v  41174  smfmullem4  41477  smflimsupmpt  41511  smfliminfmpt  41514  lincdifsn  42775
  Copyright terms: Public domain W3C validator