MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3ad2antl2 Structured version   Unicode version

Theorem 3ad2antl2 1157
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antl2  |-  ( ( ( ps  /\  ph  /\ 
ta )  /\  ch )  ->  th )

Proof of Theorem 3ad2antl2
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantlr 712 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl1 1150 1  |-  ( ( ( ps  /\  ph  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 185  df-an 369  df-3an 973
This theorem is referenced by:  fcofo  6092  cocan1  6095  ordiso2  7855  fin1a2lem9  8701  fin1a2lem12  8704  gchpwdom  8959  winainflem  8982  muldvds1  14010  ramcl  14549  gsumccat  16126  oddvdsnn0  16685  ghmplusg  16969  frlmsslss2  18894  frlmsslss2OLD  18895  frlmsslsp  18916  islindf4  18958  mamures  18977  matepmcl  19049  matepm2cl  19050  pmatcollpw2lem  19363  cnpnei  19851  ssref  20098  qtopss  20301  elfm2  20534  flffbas  20581  cnpfcf  20627  deg1ldg  22577  brbtwn2  24329  colinearalg  24334  axsegconlem1  24341  clwwlkf  24915  2spontn0vne  25008  usgreghash2spot  25190  nvmul0or  25664  hoadddi  26838  volfiniune  28358  funsseq  29364  bpolydif  29970  nn0prpwlem  30306  fnemeet1  30350  keridl  30595  lcmdvds  31382  n0p  31604  lptre2pt  31812  dvnprodlem1  31909  fourierdlem42  32097  fourierdlem48  32103  fourierdlem54  32109  fourierdlem77  32132  spthdifv  32670  bnj548  34302  pmapglbx  35906  elpaddn0  35937  paddasslem9  35965  paddasslem10  35966  cdleme42mgN  36627  relexpxpmin  38244
  Copyright terms: Public domain W3C validator